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