src/HOL/Nominal/nominal_inductive.ML

--- a/src/HOL/Nominal/nominal_inductive.ML	Tue Feb 10 14:29:36 2015 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Tue Feb 10 14:48:26 2015 +0100
@@ -130,7 +130,7 @@
     fun prove t =
       Goal.prove ctxt [] [] t (fn _ =>
         EVERY [cut_facts_tac [th] 1, etac rev_mp 1,
-          REPEAT_DETERM (FIRSTGOAL (resolve_tac monos)),
+          REPEAT_DETERM (FIRSTGOAL (resolve_tac ctxt monos)),
           REPEAT_DETERM (rtac impI 1 THEN (atac 1 ORELSE tac))])
   in Option.map prove (map_term f prop (the_default prop opt)) end;
 
@@ -296,8 +296,8 @@
               NominalDatatype.fresh_const T (fastype_of p) $
                 Bound 0 $ p)))
           (fn _ => EVERY
-            [resolve_tac exists_fresh' 1,
-             resolve_tac fs_atoms 1]);
+            [resolve_tac ctxt exists_fresh' 1,
+             resolve_tac ctxt fs_atoms 1]);
         val (([(_, cx)], ths), ctxt') = Obtain.result
           (fn ctxt' => EVERY
             [etac exE 1,
@@ -388,17 +388,17 @@
                        (simp_tac (put_simpset HOL_basic_ss ctxt''
                           addsimps [inductive_forall_def']
                           addsimprocs [NominalDatatype.perm_simproc]) 1 THEN
-                        resolve_tac gprems2 1)]));
+                        resolve_tac ctxt'' gprems2 1)]));
                  val final = Goal.prove ctxt'' [] [] (term_of concl)
                    (fn _ => cut_facts_tac [th] 1 THEN full_simp_tac (put_simpset HOL_ss ctxt''
                      addsimps vc_compat_ths'' @ freshs2' @
                        perm_fresh_fresh @ fresh_atm) 1);
                  val final' = Proof_Context.export ctxt'' ctxt' [final];
-               in resolve_tac final' 1 end) context 1])
+               in resolve_tac ctxt' final' 1 end) context 1])
                  (prems ~~ thss ~~ ihyps ~~ prems'')))
         in
           cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN
-          REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN
+          REPEAT (REPEAT (resolve_tac ctxt [conjI, impI] 1) THEN
             etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN
             asm_full_simp_tac ctxt 1)
         end) |> singleton (Proof_Context.export ctxt' ctxt);
@@ -532,10 +532,10 @@
                          in
                            simp_tac case_simpset 1 THEN
                            REPEAT_DETERM (TRY (rtac conjI 1) THEN
-                             resolve_tac case_hyps' 1)
+                             resolve_tac ctxt4 case_hyps' 1)
                          end) ctxt4 1)
                   val final = Proof_Context.export ctxt3 ctxt2 [th]
-                in resolve_tac final 1 end) ctxt1 1)
+                in resolve_tac ctxt2 final 1 end) ctxt1 1)
                   (thss ~~ hyps ~~ prems))) |>
                   singleton (Proof_Context.export ctxt' ctxt))
 
@@ -634,7 +634,7 @@
             val intr' = Drule.cterm_instantiate (map (cterm_of thy) vs ~~
                map (cterm_of thy o NominalDatatype.mk_perm [] pi o term_of o #2) params)
                intr
-          in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac prems'')) 1
+          in (rtac intr' THEN_ALL_NEW (TRY o resolve_tac ctxt'' prems'')) 1
           end) ctxt' 1 st
       in
         case (Seq.pull res handle THM (s, _, _) => eqvt_err s) of