diff -r 005e4edc65ef -r cd4226736c37 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Dec 08 17:43:32 2009 +0100
+++ b/Quot/QuotMain.thy	Tue Dec 08 20:34:00 2009 +0100
@@ -1043,10 +1043,11 @@
 (* 1. conversion (is not a pattern) *)
 thm lambda_prs
 (* 2. folding of definitions: (rep ---> abs) oldConst == newconst *)
+(*    prservation lemma                                           *)
 (*    and simplification with                                     *)
 thm all_prs ex_prs 
 (* 3. simplification with *)
-thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps
+thm fun_map.simps Quotient_abs_rep Quotient_rel_rep id_simps 
 (* 4. Test for refl *)
 
 ML {*