src/HOL/Word/Word.thy
changeset 46136 a3d4cf5203f5
parent 46124 3ee75fe01986
child 46172 c06e868dc339
--- a/src/HOL/Word/Word.thy	Fri Jan 06 15:19:17 2012 +0100
+++ b/src/HOL/Word/Word.thy	Fri Jan 06 16:42:15 2012 +0100
@@ -116,7 +116,8 @@
   "word_int_case f w = f (uint w)"
 
 translations
-  "case x of CONST of_int y => b" == "CONST word_int_case (%y. b) x"
+  "case x of XCONST of_int y => b" == "CONST word_int_case (%y. b) x"
+  "case x of (XCONST of_int :: 'a) y => b" => "CONST word_int_case (%y. b) x"
 
 subsection {* Type-definition locale instantiations *}