Mercurial Mercurial > hg > nominal2 / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/quotient_tacs.ML
changeset 939 ce774af6b964
parent 930 68c1f378a70a
child 940 a792bfc1be2b 
--- 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