src/HOL/String.thy
changeset 38858 1920158cfa17
parent 38808 89ae86205739
parent 38857 97775f3e8722
child 39198 f967a16dfcdd
--- a/src/HOL/String.thy	Fri Aug 27 22:30:25 2010 +0200
+++ b/src/HOL/String.thy	Sat Aug 28 11:42:33 2010 +0200
@@ -183,10 +183,10 @@
   fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
 *}
 
-code_instance literal :: eq
+code_instance literal :: equal
   (Haskell -)
 
-code_const "eq_class.eq \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
   (SML "!((_ : string) = _)")
   (OCaml "!((_ : string) = _)")
   (Haskell infixl 4 "==")