diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Library/Code_Integer.thy
--- a/src/HOL/Library/Code_Integer.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/Code_Integer.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -21,7 +21,7 @@
   (Scala "BigInt")
   (Eval "int")
 
-code_instance int :: eq
+code_instance int :: equal
   (Haskell -)
 
 setup {*
@@ -96,7 +96,7 @@
   (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
   (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
 
-code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
   (SML "!((_ : IntInf.int) = _)")
   (OCaml "Big'_int.eq'_big'_int")
   (Haskell infixl 4 "==")