diff -r 03ca07d478be -r a1937c51ed88 src/HOL/Code_Generator.thy
--- a/src/HOL/Code_Generator.thy	Wed Nov 22 10:20:11 2006 +0100
+++ b/src/HOL/Code_Generator.thy	Wed Nov 22 10:20:12 2006 +0100
@@ -192,13 +192,8 @@
 
 subsubsection {* eq class *}
 
-class eq =
-  fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-
-defs
-  eq_def [normal post]: "eq \<equiv> (op =)"
-
-lemmas [symmetric, code inline, code func] = eq_def
+axclass eq \<subseteq> type
+  attach "op ="
 
 
 subsubsection {* bool type *}
@@ -206,36 +201,36 @@
 instance bool :: eq ..
 
 lemma [code func]:
-  "eq True p = p" unfolding eq_def by auto
+  "True = P \<longleftrightarrow> P" by simp
 
 lemma [code func]:
-  "eq False p = (\<not> p)" unfolding eq_def by auto
+  "False = P \<longleftrightarrow> \<not> P" by simp
 
 lemma [code func]:
-  "eq p True = p" unfolding eq_def by auto
+  "P = True \<longleftrightarrow> P" by simp
 
 lemma [code func]:
-  "eq p False = (\<not> p)" unfolding eq_def by auto
+  "P = False \<longleftrightarrow> \<not> P" by simp
 
 
 subsubsection {* Haskell *}
 
 code_class eq
-  (Haskell "Eq" where eq \<equiv> "(==)")
+  (Haskell "Eq" where "op =" \<equiv> "(==)")
 
-code_const eq
+code_const "op ="
   (Haskell infixl 4 "==")
 
 code_instance bool :: eq
   (Haskell -)
 
-code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
+code_const "op = \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
 code_reserved Haskell
   Eq eq
 
 
-hide (open) const eq if_delayed
+hide (open) const if_delayed
 
 end
\ No newline at end of file