diff -r a2f3f523c84b -r a751bec7cf29 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Fri Jul 21 14:48:17 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy	Fri Jul 21 14:48:35 2006 +0200
@@ -908,22 +908,19 @@
 
 code_constapp
   "op + :: int \<Rightarrow> int \<Rightarrow> int"
-    ml (infixl 8 "+")
+    ml ("IntInf.+ (_, _)")
     haskell (infixl 6 "+")
   "op * :: int \<Rightarrow> int \<Rightarrow> int"
-    ml (infixl 9 "*")
+    ml ("IntInf.* (_, _)")
     haskell (infixl 7 "*")
   "uminus :: int \<Rightarrow> int"
     ml (target_atom "~")
     haskell (target_atom "negate")
   "op = :: int \<Rightarrow> int \<Rightarrow> bool"
-    ml (infixl 6 "=")
+    ml ("(op =) (_ : IntInf.int, _)")
     haskell (infixl 4 "==")
-  "op < :: int \<Rightarrow> int \<Rightarrow> bool"
-    ml (infix 6 "<")
-    haskell (infix 4 "<")
   "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
-    ml (infix 6 "<=")
+    ml ("IntInf.<= (_, _)")
     haskell (infix 4 "<=")
 
 ML {*
@@ -960,7 +957,6 @@
 setup {*
   Codegen.add_codegen "number_of_codegen" number_of_codegen
   (* #> CodegenPackage.add_appconst ("Numeral.number_of", appgen_number) *)
-  #> CodegenPackage.set_int_tyco "IntDef.int"
 *}
 
 quickcheck_params [default_type = int]