--- a/Nominal/nominal_mutual.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_mutual.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -19,7 +19,7 @@
     -> term list
     -> local_theory
     -> ((thm (* goalstate *)
-        * (thm -> Nominal_Function_Common.nominal_function_result) (* proof continuation *)
+        * (Proof.context -> thm -> Nominal_Function_Common.nominal_function_result) (* proof continuation *)
        ) * local_theory)
 end
 
@@ -330,21 +330,23 @@
 
     val induct_thm = case induct_thms of
         [thm] => thm
-          |> Drule.gen_all (Variable.maxidx_of ctxt')
+          |> Variable.gen_all ctxt'
           |> Thm.permute_prems 0 1
           |> (fn thm => atomize_rule ctxt' (length (Thm.prems_of thm) - 1) thm)
       | thms => thms
-          |> map (Drule.gen_all (Variable.maxidx_of ctxt'))
+          |> map (Variable.gen_all ctxt')
           |> map (Rule_Cases.add_consumes 1)
           |> snd o Rule_Cases.strict_mutual_rule ctxt'
           |> atomize_concl ctxt'
 
     fun tac ctxt thm =
-      rtac (Drule.gen_all (Variable.maxidx_of ctxt) thm) THEN_ALL_NEW assume_tac ctxt
+      resolve_tac ctxt [Variable.gen_all ctxt thm]
+        THEN_ALL_NEW assume_tac ctxt
   in
     Goal.prove ctxt' (flat arg_namess) [] goal
       (fn {context = ctxt'', ...} =>
-        HEADGOAL (DETERM o (rtac induct_thm) THEN' RANGE (map (tac ctxt'') eqvts_thms)))
+        HEADGOAL (DETERM o (resolve_tac ctxt'' [induct_thm]) THEN'
+          RANGE (map (tac ctxt'') eqvts_thms)))
     |> singleton (Proof_Context.export ctxt' ctxt)
     |> split_conj_thm
     |> map (fn th => th RS mp)
@@ -441,7 +443,7 @@
     val ((G_aux, GIntro_aux_thms, _, G_aux_induct), lthy''') = 
       Nominal_Function_Core.inductive_def ((Binding.name G_name_aux, G_type), NoSyn) GIntros_aux lthy''
 
-    val mutual_cont = mk_partial_rules_mutual lthy''' cont mutual'
+    fun mutual_cont ctxt = mk_partial_rules_mutual lthy''' (cont ctxt) mutual'
 
     (* proof of equivalence between graph and auxiliary graph *)
     val x = Var(("x", 0), ST)
@@ -474,22 +476,25 @@
     val simpset1 = put_simpset HOL_ss lthy''' addsimps simp_thms
 
     val inj_thm = Goal.prove lthy''' [] [] goal_inj 
-      (K (HEADGOAL (DETERM o etac G_aux_induct THEN_ALL_NEW asm_simp_tac simpset1)))
+      (K (HEADGOAL (DETERM o eresolve_tac lthy''' [G_aux_induct]
+        THEN_ALL_NEW asm_simp_tac simpset1)))
 
     fun aux_tac thm = 
-      rtac (Drule.gen_all (Variable.maxidx_of lthy''') thm) THEN_ALL_NEW
+      resolve_tac lthy''' [Variable.gen_all lthy''' thm] THEN_ALL_NEW
       asm_full_simp_tac (simpset1 addsimps [inj_thm])
     
     val iff1_thm = Goal.prove lthy''' [] [] goal_iff1 
-      (K (HEADGOAL (DETERM o etac G_aux_induct THEN' RANGE (map aux_tac GIntro_thms))))
-      |> Drule.gen_all (Variable.maxidx_of lthy''')
+      (K (HEADGOAL (DETERM o eresolve_tac lthy''' [G_aux_induct]
+        THEN' RANGE (map aux_tac GIntro_thms))))
+      |> Variable.gen_all lthy'''
     val iff2_thm = Goal.prove lthy''' [] [] goal_iff2 
-      (K (HEADGOAL (DETERM o etac G_induct THEN' RANGE
+      (K (HEADGOAL (DETERM o eresolve_tac lthy''' [G_induct] THEN' RANGE
         (map (aux_tac o simplify simpset0) GIntro_aux_thms))))
-      |> Drule.gen_all (Variable.maxidx_of lthy''')
+      |> Variable.gen_all lthy'''
 
     val iff_thm = Goal.prove lthy''' [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (G, G_aux)))
-      (K (HEADGOAL (EVERY' ((map rtac @{thms ext ext iffI}) @ [etac iff2_thm, etac iff1_thm]))))
+      (K (HEADGOAL (EVERY' ((map (resolve_tac lthy''' o single) @{thms ext ext iffI}) @
+        [eresolve_tac lthy''' [iff2_thm], eresolve_tac lthy''' [iff1_thm]]))))
  
     val tac = HEADGOAL (simp_tac (put_simpset HOL_basic_ss lthy''' addsimps [iff_thm]))
     val goalstate' =