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.
Nominal/nominal_termination.ML
changeset 3218 89158f401b07
parent 3193 87d1e815aa59
child 3227 35bb5b013f0e 
--- a/Nominal/nominal_termination.ML	Mon Apr 01 23:22:53 2013 +0100
+++ b/Nominal/nominal_termination.ML	Fri Apr 19 00:10:52 2013 +0100
@@ -49,7 +49,8 @@
         let
           val totality = Thm.close_derivation totality
           val remove_domain_condition =
-            full_simplify (HOL_basic_ss addsimps [totality, @{thm True_implies_equals}])
+            full_simplify (put_simpset HOL_basic_ss lthy
+              addsimps [totality, @{thm True_implies_equals}])
           val tsimps = map remove_domain_condition psimps
           val tinducts = map remove_domain_condition pinducts
           val teqvts = map remove_domain_condition eqvts
nominal2