Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Changed the lambda_prs_simple_conv to use id_apply, now last eq_reflection can be removed from id_simps.
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Tue, 26 Jan 2010 12:24:23 +0100
changeset 939 ce774af6b964
parent 938 0ff855a6ffb7
child 940 a792bfc1be2b
Changed the lambda_prs_simple_conv to use id_apply, now last eq_reflection can be removed from id_simps.
Quot/QuotMain.thy file | annotate | diff | comparison | revisions
Quot/quotient_tacs.ML file | annotate | diff | comparison | revisions 
--- 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
--- 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)
nominal2