# HG changeset patch
# User wenzelm
# Date 1325864535 -3600
# Node ID a3d4cf5203f553917c74243debdfa18a5bbe6ed0
# Parent  6bff2ebaf7bbbceb2194fea0e685f1ed4c5d309d
recovered case syntax for of_int, also with source positions (appears to be unused nonetheless);

diff -r 6bff2ebaf7bb -r a3d4cf5203f5 src/HOL/Word/Word.thy
--- 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 *}