| 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 *}