# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264505063 -3600
# Node ID ce774af6b9648c930567c489707cde5b3714b92b
# Parent  0ff855a6ffb7f4a63fe5c68a340874dfb4512aa4
Changed the lambda_prs_simple_conv to use id_apply, now last eq_reflection can be removed from id_simps.

diff -r 0ff855a6ffb7 -r ce774af6b964 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Tue Jan 26 12:06:47 2010 +0100
+++ b/Quot/QuotMain.thy	Tue Jan 26 12:24:23 2010 +0100
@@ -112,7 +112,7 @@
 lemmas [id_simps] =
   id_def[symmetric]
   fun_map_id
-  id_apply[THEN eq_reflection]
+  id_apply
   id_o
   o_id
   eq_comp_r
diff -r 0ff855a6ffb7 -r ce774af6b964 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Tue Jan 26 12:06:47 2010 +0100
+++ b/Quot/quotient_tacs.ML	Tue Jan 26 12:24:23 2010 +0100
@@ -486,7 +486,7 @@
         val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
         val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
         val te = solve_quotient_assm ctxt (solve_quotient_assm ctxt lpi)
-        val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
+        val ts = MetaSimplifier.rewrite_rule @{thms id_apply[THEN eq_reflection]} te
         val (insp, inst) =
           if ty_c = ty_d
           then make_inst_id (term_of (Thm.lhs_of ts)) (term_of ctrm)