--- a/src/HOL/Library/Code_Natural.thy Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/Code_Natural.thy Fri Aug 27 19:34:23 2010 +0200
@@ -112,7 +112,7 @@
false Code_Printer.literal_alternative_numeral) ["Haskell", "Scala"]
*}
-code_instance code_numeral :: eq
+code_instance code_numeral :: equal
(Haskell -)
code_const "op + \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> code_numeral"
@@ -131,7 +131,7 @@
(Haskell "divMod")
(Scala infixl 8 "/%")
-code_const "eq_class.eq \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
(Haskell infixl 4 "==")
(Scala infixl 5 "==")