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

diff -r e78db03b4e11 -r a0f50b34765c Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Wed Dec 09 15:28:01 2009 +0100
+++ b/Quot/QuotMain.thy	Wed Dec 09 15:29:36 2009 +0100
@@ -1053,7 +1053,7 @@
 (*    bound variables                                  *)
 thm fun_map.simps
 (* 3. simplification with *)
-lambda_prs
+thm lambda_prs
 (* 4. simplification with *)
 thm Quotient_abs_rep Quotient_rel_rep id_simps 
 (* 5. Test for refl *)