[isabelle-dev] Strange behavior in Word library

[John Matthews]

If I turn on "show types" in Isabelle_19-Nov-2007 and run the  
following commands:

   theory WordTest imports WordMain
   begin

   lemma "P (ucast ((0b1110 :: 4 word) >> 1) :: 2 word)"
   apply simp

Isabelle displays the simplified subgoal as:

   goal (1 subgoal):
    1. P (7::2 word)
   variables:
    P :: 2 word :: bool

Notice the subterm "7::2 word" showing up in the subgoal, which isn't  
right. On the other hand, the formula

   lemma "(ucast ((0b1110 :: 4 word) >> 1) :: 2 word) = 0b11"
   by simp

is proved without problems. So it seems there is a bug in the way  
word constants are printed out.

Thanks,
-john