diff -r 4562584d9d66 -r b8390cd56b8f src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/HOL.thy	Thu Sep 25 09:28:03 2008 +0200
@@ -1710,16 +1710,24 @@
 
 class eq = type +
   fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-  assumes eq: "eq x y \<longleftrightarrow> x = y "
+  assumes eq_equals: "eq x y \<longleftrightarrow> x = y "
 begin
 
+lemma eq: "eq = (op =)"
+  by (rule ext eq_equals)+
+
 lemma equals_eq [code inline, code func]: "op = \<equiv> eq"
-  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq)
+  by (rule eq_reflection) (rule ext, rule ext, rule sym, rule eq_equals)
 
 declare equals_eq [symmetric, code post]
 
+lemma eq_refl: "eq x x \<longleftrightarrow> True"
+  unfolding eq by rule+
+
 end
 
+declare simp_thms(6) [code nbe]
+
 hide (open) const eq
 hide const eq