src/HOL/Library/Code_Natural.thy
changeset 38857 97775f3e8722
parent 38810 361119ea62ee
child 38968 e55deaa22fff
--- 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 "==")