The typed print translation in Numeral_Type.thy, which prints "card
(UNIV :: 'a set)" as "CARD('a)", is broken.
I think it has something to do with the new properly-qualified name
for "UNIV" that was introduced recently.
Anyway, I'm not exactly sure what is going wrong or how to fix it.
Does anyone have an idea?
- Brian