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 *)