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_dt_rawfuns.ML
changeset 3226 780b7a2c50b6
parent 3218 89158f401b07
child 3239 67370521c09c 
--- a/Nominal/nominal_dt_rawfuns.ML	Mon Oct 14 11:23:18 2013 +0200
+++ b/Nominal/nominal_dt_rawfuns.ML	Sun Dec 15 15:14:40 2013 +1100
@@ -467,7 +467,7 @@
 
 fun prove_eqvt_tac insts ind_thms const_names simps ctxt = 
   HEADGOAL
-    (Object_Logic.full_atomize_tac
+    (Object_Logic.full_atomize_tac ctxt
      THEN' (DETERM o (Induct_Tacs.induct_rules_tac ctxt insts ind_thms))  
      THEN_ALL_NEW  subproof_tac const_names simps ctxt)
nominal2