Дмитро, can you expand a bit on how you prove that every ℵ<sub>α+ω</sub> is measurable in the HOD of L[Card] and why the sequence of the ℵ<sub>α+n</sub>s is Prikry generic, assuming there is a sharp for an inner model with a proper class of measurable cardinals? Thanks, Ralf. Regardless of that, the result is correct: if L[Card] doesn't have an inner model with a proper class of measurable cardinals, then we may compare K<sup>L[Card]</sup> with the sharp for an inner model with a proper class of measurable cardinals; a half-open interval from Card may then be used to produce a measure on an iterate of K<sup>L[Card]</sup> which may be pulled back to K<sup>L[Card]</sup>; this measure is in L[Card], which gives a contradiction. Your question about the complexity of the reals of L[cf] is related to the question: which reals does C* have (where C* is the least inner model which knows which ordinals have countable cofinality)? Magidor showed C* has 0<sup>†</sup> and more, and with him I showed (assuming a measurable cardinal above a Woodin cardinal in V) that all the reals of C* are in M<sub>1</sub>, the least inner model with one Wodin cardinal (so that K<sup>C*</sup> exists and is 1-small).