recovered case syntax for of_int, also with source positions (appears to be unused nonetheless);

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