--- a/Quot/QuotBase.thy	Tue Jan 26 01:42:46 2010 +0100
+++ b/Quot/QuotBase.thy	Tue Jan 26 10:53:44 2010 +0100
@@ -72,11 +72,9 @@
 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)
-  apply (rule ext)+
-  apply auto
-  done
+lemma eq_comp_r: 
+  shows "((op =) OOO R) = R"
+  by (auto simp add: expand_fun_eq)
 
 section {* Respects predicate *}
 
@@ -108,8 +106,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)"
@@ -396,10 +394,9 @@
 lemma babs_prs:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
-  shows "(Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f)) \<equiv> f"
-  apply(rule eq_reflection)
-  apply(rule ext)
-  apply simp
+  shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
+  apply (rule ext)
+  apply (simp)
   apply (subgoal_tac "Rep1 x \<in> Respects R1")
   apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
   apply (simp add: in_respects Quotient_rel_rep[OF q1])