--- a/QuotScript.thy	Sat Oct 17 15:42:57 2009 +0200
+++ b/QuotScript.thy	Sat Oct 17 16:06:54 2009 +0200
@@ -81,8 +81,8 @@
 by auto
 
 lemma IDENTITY_QUOTIENT:
-  shows "QUOTIENT (op =) (\<lambda>x. x) (\<lambda>x. x)"
-unfolding QUOTIENT_def
+  shows "QUOTIENT (op =) id id"
+unfolding QUOTIENT_def id_def
 by blast
 
 lemma QUOTIENT_SYM:
@@ -114,8 +114,8 @@
   "f ---> g \<equiv> fun_map f g"
 
 lemma FUN_MAP_I:
-  shows "((\<lambda>x. x) ---> (\<lambda>x. x)) = (\<lambda>x. x)"
-by (simp add: expand_fun_eq)
+  shows "(id ---> id) = id"
+by (simp add: expand_fun_eq id_def)
 
 lemma IN_FUN:
   shows "x \<in> ((f ---> g) s) = g (f x \<in> s)"
@@ -382,13 +382,13 @@
 
 lemma I_PRS:
   assumes q: "QUOTIENT R Abs Rep"
-  shows "(\<lambda>x. x) e = Abs ((\<lambda> x. x) (Rep e))"
+  shows "id e = Abs (id (Rep e))"
 using QUOTIENT_ABS_REP[OF q] by auto
 
 lemma I_RSP:
   assumes q: "QUOTIENT R Abs Rep"
   and     a: "R e1 e2"
-  shows "R ((\<lambda>x. x) e1) ((\<lambda> x. x) e2)"
+  shows "R (id e1) (id e2)"
 using a by auto
 
 lemma o_PRS: