# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260368881 -3600
# Node ID e78db03b4e11d3cd008a07ad66814ee3195cfd22
# Parent  86c60d55373c79c57c0facd1a10e71690f3ce20b
tuned

diff -r 86c60d55373c -r e78db03b4e11 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Wed Dec 09 15:24:11 2009 +0100
+++ b/Quot/QuotMain.thy	Wed Dec 09 15:28:01 2009 +0100
@@ -1051,10 +1051,12 @@
 thm babs_prs all_prs ex_prs 
 (* 2. unfolding of ---> in front of everything, except *)
 (*    bound variables                                  *)
-thm fun_map_simps
+thm fun_map.simps
 (* 3. simplification with *)
+lambda_prs
+(* 4. simplification with *)
 thm Quotient_abs_rep Quotient_rel_rep id_simps 
-(* 4. Test for refl *)
+(* 5. Test for refl *)
 
 ML {*
 fun clean_tac lthy =