--- a/Quot/QuotBase.thy	Mon Jan 25 20:47:20 2010 +0100
+++ b/Quot/QuotBase.thy	Tue Jan 26 07:14:10 2010 +0100
@@ -72,8 +72,7 @@
 where
   "r1 OOO r2 \<equiv> r1 OO r2 OO r1"
 
-lemma eq_comp_r: "op = OO R OO op = \<equiv> R"
-  apply (rule eq_reflection)
+lemma eq_comp_r: "(op = OO R OO op =) = R"
   apply (rule ext)+
   apply auto
   done
@@ -108,8 +107,8 @@
   by (simp add: expand_fun_eq id_def)
 
 lemma fun_rel_eq:
-  shows "(op =) ===> (op =) \<equiv> (op =)"
-  by (rule eq_reflection) (simp add: expand_fun_eq)
+  shows "((op =) ===> (op =)) = (op =)"
+  by (simp add: expand_fun_eq)
 
 lemma fun_rel_id:
   assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"