1.1 --- a/src/HOL/Word/Word.thy	Fri Jan 06 15:19:17 2012 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Fri Jan 06 16:42:15 2012 +0100
     1.3 @@ -116,7 +116,8 @@
     1.4    "word_int_case f w = f (uint w)"
     1.5  
     1.6  translations
     1.7 -  "case x of CONST of_int y => b" == "CONST word_int_case (%y. b) x"
     1.8 +  "case x of XCONST of_int y => b" == "CONST word_int_case (%y. b) x"
     1.9 +  "case x of (XCONST of_int :: 'a) y => b" => "CONST word_int_case (%y. b) x"
    1.10  
    1.11  subsection {* Type-definition locale instantiations *}
    1.12