diff -r e30997c88050 -r e169a99c6ada QuotScript.thy
--- a/QuotScript.thy	Fri Oct 30 19:03:53 2009 +0100
+++ b/QuotScript.thy	Sat Oct 31 11:20:55 2009 +0100
@@ -274,7 +274,7 @@
 lemma LAMBDA_PRS:
   assumes q1: "QUOTIENT R1 Abs1 Rep1"
   and     q2: "QUOTIENT R2 Abs2 Rep2"
-  shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x)))"
+  shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
 unfolding expand_fun_eq
 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]
 by simp
@@ -284,7 +284,16 @@
   and     q2: "QUOTIENT R2 Abs2 Rep2"
   shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x)"
 unfolding expand_fun_eq
-by (subst LAMBDA_PRS[OF q1 q2]) (simp)
+using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]
+by (simp)
+
+lemma APP_PRS:
+  assumes q1: "QUOTIENT R1 abs1 rep1"
+  and     q2: "QUOTIENT R2 abs2 rep2"
+  shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x"
+unfolding expand_fun_eq
+using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2]
+by simp
 
 (* Ask Peter: assumption q1 and q2 not used and lemma is the 'identity' *)
 lemma LAMBDA_RSP: