1.1 --- a/src/HOL/Word/Word.thy	Tue Dec 27 12:27:06 2011 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Tue Dec 27 12:37:11 2011 +0100
     1.3 @@ -115,8 +115,6 @@
     1.4  definition word_int_case :: "(int => 'b) => ('a :: len0 word) => 'b" where
     1.5    "word_int_case f w = f (uint w)"
     1.6  
     1.7 -syntax
     1.8 -  of_int :: "int => 'a"
     1.9  translations
    1.10    "case x of CONST of_int y => b" == "CONST word_int_case (%y. b) x"
    1.11