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 828 e1f1114ae8bd
parent 826 e3732ed89dfc
child 837 116c7a30e0a2 
--- a/Quot/quotient_tacs.ML	Fri Jan 08 11:20:12 2010 +0100
+++ b/Quot/quotient_tacs.ML	Fri Jan 08 14:43:30 2010 +0100
@@ -158,7 +158,7 @@
   val bex_pat  = @{term "Bex (Respects (R1 ===> R2)) P"}
   val simproc = Simplifier.simproc_i thy "" [ball_pat, bex_pat] (K (ball_bex_range_simproc))
   val simpset = (mk_minimal_ss ctxt) 
-                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp id_simps}
+                       addsimps @{thms ball_reg_eqv bex_reg_eqv babs_reg_eqv babs_simp} @ (id_simps_get ctxt)
                        addsimprocs [simproc] 
                        addSolver equiv_solver addSolver quotient_solver
   val eq_eqvs = map (OF1 @{thm eq_imp_rel}) (equiv_rules_get ctxt)
nominal2