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_mutual.ML
changeset 3226 780b7a2c50b6
parent 3219 e5d9b6bca88c
child 3227 35bb5b013f0e 
--- a/Nominal/nominal_mutual.ML	Mon Oct 14 11:23:18 2013 +0200
+++ b/Nominal/nominal_mutual.ML	Sun Dec 15 15:14:40 2013 +1100
@@ -335,12 +335,12 @@
         [thm] => thm
           |> Drule.gen_all 
           |> Thm.permute_prems 0 1
-          |> (fn thm => atomize_rule (length (prems_of thm) - 1) thm)
+          |> (fn thm => atomize_rule ctxt' (length (prems_of thm) - 1) thm)
       | thms => thms
           |> map Drule.gen_all 
           |> map (Rule_Cases.add_consumes 1)
           |> snd o Rule_Cases.strict_mutual_rule ctxt'
-          |> atomize_concl
+          |> atomize_concl ctxt'
 
     fun tac thm = rtac (Drule.gen_all thm) THEN_ALL_NEW atac
   in
nominal2