src/HOL/Library/Code_Char.thy
changeset 38857 97775f3e8722
parent 37459 7a3610dca96b
child 39250 548a3e5521ab
--- a/src/HOL/Library/Code_Char.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Library/Code_Char.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -19,7 +19,7 @@
   #> String_Code.add_literal_list_string "Haskell"
 *}
 
-code_instance char :: eq
+code_instance char :: equal
   (Haskell -)
 
 code_reserved SML
@@ -31,7 +31,7 @@
 code_reserved Scala
   char
 
-code_const "eq_class.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   (SML "!((_ : char) = _)")
   (OCaml "!((_ : char) = _)")
   (Haskell infixl 4 "==")