src/HOL/Nominal/nominal_inductive.ML

              REPEAT (etac conjE 1)])
           [ex] ctxt
       in (freshs1 @ [term_of cx], freshs2 @ ths, ctxt') end;
 
     fun mk_ind_proof thy thss =
-      let val ctxt = ProofContext.init thy
-      in Goal.prove_global thy [] prems' concl' (fn ihyps =>
+      Goal.prove_global thy [] prems' concl' (fn {prems = ihyps, context = ctxt} =>
         let val th = Goal.prove ctxt [] [] concl (fn {context, ...} =>
           rtac raw_induct 1 THEN
           EVERY (maps (fn ((((_, bvars, oprems, _), vc_compat_ths), ihyp), (vs, ihypt)) =>
             [REPEAT (rtac allI 1), simp_tac eqvt_ss 1,
              SUBPROOF (fn {prems = gprems, params, concl, context = ctxt', ...} =>

         in
           cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN
           REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN
             etac impE 1 THEN atac 1 THEN REPEAT (etac allE_Nil 1) THEN
             asm_full_simp_tac (simpset_of thy) 1)
-        end)
-      end;
+        end);
 
     (** strong case analysis rule **)
 
     val cases_prems = map (fn ((name, avoids), rule) =>
       let

 
     val cases_eqvt_ss = HOL_ss addsimps eqvt_thms @ calc_atm delsplits [split_if];
 
     fun mk_cases_proof thy ((((name, thss), elim), (prem, args, concl, prems)),
         prems') =
-      let val ctxt1 = ProofContext.init thy
-      in (name, Goal.prove_global thy [] (prem :: prems') concl (fn hyp :: hyps =>
+      (name, Goal.prove_global thy [] (prem :: prems') concl
+        (fn {prems = hyp :: hyps, context = ctxt1} =>
         EVERY (rtac (hyp RS elim) 1 ::
           map (fn (((_, vc_compat_ths), case_hyp), (_, qs, is, _)) =>
             SUBPROOF (fn {prems = case_hyps, params, context = ctxt2, concl, ...} =>
               if null qs then
                 rtac (first_order_mrs case_hyps case_hyp) 1

                              resolve_tac case_hyps' 1)
                          end) ctxt4 1)
                   val final = ProofContext.export ctxt3 ctxt2 [th]
                 in resolve_tac final 1 end) ctxt1 1)
                   (thss ~~ hyps ~~ prems))))
-      end
 
   in
     thy |>
     ProofContext.init |>
     Proof.theorem_i NONE (fn thss => ProofContext.theory (fn thy =>