--- a/src/HOL/Option.thy Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Option.thy Fri Aug 27 19:34:23 2010 +0200
@@ -99,8 +99,8 @@
by (simp add: is_none_def)
lemma [code_unfold]:
- "eq_class.eq x None \<longleftrightarrow> is_none x"
- by (simp add: eq is_none_none)
+ "HOL.equal x None \<longleftrightarrow> is_none x"
+ by (simp add: equal is_none_none)
hide_const (open) is_none
@@ -116,10 +116,10 @@
(Haskell "Nothing" and "Just")
(Scala "!None" and "Some")
-code_instance option :: eq
+code_instance option :: equal
(Haskell -)
-code_const "eq_class.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
+code_const "HOL.equal \<Colon> 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
(Haskell infixl 4 "==")
code_reserved SML