--- a/Quot/QuotScript.thy	Thu Jan 21 10:55:09 2010 +0100
+++ b/Quot/QuotScript.thy	Thu Jan 21 11:11:22 2010 +0100
@@ -468,7 +468,8 @@
 
 lemma ex1_prs:
   assumes a: "Quotient R absf repf"
-  shows "Bexeq R ((absf ---> id) f) = Ex1 f"
+  shows "((absf ---> id) ---> id) (Bexeq R) f = Ex1 f"
+apply simp
 apply (subst Bexeq_def)
 apply (subst Bex_def)
 apply (subst Ex1_def)