--- a/Quot/QuotBase.thy	Tue Jan 26 07:14:10 2010 +0100
+++ b/Quot/QuotBase.thy	Tue Jan 26 07:42:52 2010 +0100
@@ -395,10 +395,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])