--- a/src/HOL/List.thy Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/List.thy Fri Aug 27 19:34:23 2010 +0200
@@ -4721,8 +4721,8 @@
by (simp add: null_def)
lemma equal_Nil_null [code_unfold]:
- "eq_class.eq xs [] \<longleftrightarrow> null xs"
- by (simp add: eq eq_Nil_null)
+ "HOL.equal xs [] \<longleftrightarrow> null xs"
+ by (simp add: equal eq_Nil_null)
definition maps :: "('a \<Rightarrow> 'b list) \<Rightarrow> 'a list \<Rightarrow> 'b list" where
[code_post]: "maps f xs = concat (map f xs)"
@@ -4821,10 +4821,10 @@
(Haskell "[]")
(Scala "!Nil")
-code_instance list :: eq
+code_instance list :: equal
(Haskell -)
-code_const "eq_class.eq \<Colon> 'a\<Colon>eq list \<Rightarrow> 'a list \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
(Haskell infixl 4 "==")
code_reserved SML