diff -r 92ef83e5eaea -r 9502ce541f01 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Jan 30 08:20:06 2006 +0100
+++ b/src/HOL/Orderings.thy	Mon Jan 30 08:20:56 2006 +0100
@@ -706,7 +706,7 @@
 subsection {* Code generator setup *}
 
 code_alias
-  "op <=" "Orderings.op_le"
-  "op <" "Orderings.op_lt"
+  "op <=" "IntDef.op_le"
+  "op <" "IntDef.op_lt"
 
 end