diff -r 4af8a92396ce -r a44479bde681 Nominal/nominal_inductive.ML
--- a/Nominal/nominal_inductive.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_inductive.ML	Tue Mar 22 12:18:30 2016 +0000
@@ -24,11 +24,11 @@
 fun mk_cminus p =
   Thm.apply @{cterm "uminus :: perm => perm"} p
 
-fun minus_permute_intro_tac p =
-  rtac (Drule.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE})
+fun minus_permute_intro_tac ctxt p =
+  resolve_tac ctxt [Thm.instantiate' [] [SOME (mk_cminus p)] @{thm permute_boolE}]
 
 fun minus_permute_elim p thm =
-  thm RS (Drule.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI})
+  thm RS (Thm.instantiate' [] [NONE, SOME (mk_cminus p)] @{thm permute_boolI})
 
 (* fixme: move to nominal_library *)
 fun real_head_of (@{term Trueprop} $ t) = real_head_of t
@@ -156,23 +156,23 @@
 val all_elims = 
   let
     fun spec' ct =
-      Drule.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec}
+      Thm.instantiate' [SOME (Thm.ctyp_of_cterm ct)] [NONE, SOME ct] @{thm spec}
   in
     fold (fn ct => fn th => th RS spec' ct)
   end
 
 fun helper_tac flag prm p ctxt =
-  Subgoal.SUBPROOF (fn {context, prems, ...} =>
+  Subgoal.SUBPROOF (fn {context = ctxt', prems, ...} =>
     let
       val prems' = prems
         |> map (minus_permute_elim p)
-        |> map (eqvt_srule context)
+        |> map (eqvt_srule ctxt')
 
       val prm' = (prems' MRS prm)
         |> flag ? (all_elims [p])
-        |> flag ? (eqvt_srule context)
+        |> flag ? (eqvt_srule ctxt')
     in
-      asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps (prm' :: @{thms HOL.induct_forall_def})) 1
+      asm_full_simp_tac (put_simpset HOL_ss ctxt' addsimps (prm' :: @{thms HOL.induct_forall_def})) 1
     end) ctxt
 
 fun non_binder_tac prem intr_cvars Ps ctxt = 
@@ -183,15 +183,15 @@
       val cperms = map (Thm.cterm_of ctxt' o perm_const) prm_tys
       val p_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 p ct2) cperms prms 
       val prem' = prem
-        |> cterm_instantiate (intr_cvars ~~ p_prms) 
-        |> eqvt_srule ctxt
+        |> infer_instantiate ctxt' (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ p_prms) 
+        |> eqvt_srule ctxt'
 
       (* for inductive-premises*)
       fun tac1 prm = helper_tac true prm p ctxt'
 
       (* for non-inductive premises *)   
       fun tac2 prm =  
-        EVERY' [ minus_permute_intro_tac p, 
+        EVERY' [ minus_permute_intro_tac ctxt' p, 
                  eqvt_stac ctxt', 
                  helper_tac false prm p ctxt' ]
 
@@ -199,7 +199,7 @@
         (if member same_name Ps (real_head_of t) then tac1 prm else tac2 prm) i
     in
       EVERY1 [ eqvt_stac ctxt', 
-               rtac prem', 
+               resolve_tac ctxt' [prem'], 
                RANGE (map (SUBGOAL o select) prems) ]
     end) ctxt
 
@@ -217,8 +217,9 @@
     val simp = asm_full_simp_tac (put_simpset HOL_ss ctxt addsimps ss)
   in 
     Goal.prove ctxt [] [] fresh_goal
-      (K (HEADGOAL (rtac @{thm at_set_avoiding2} 
-          THEN_ALL_NEW EVERY' [cut_facts_tac user_thm, REPEAT o etac @{thm conjE}, simp])))
+      (K (HEADGOAL (resolve_tac ctxt @{thms at_set_avoiding2}
+          THEN_ALL_NEW EVERY' [cut_facts_tac user_thm, REPEAT o
+            eresolve_tac ctxt @{thms conjE}, simp])))
   end
 
 val supp_perm_eq' = @{lemma "fresh_star (supp (permute p x)) q ==> permute p x == permute (q + p) x" 
@@ -238,27 +239,27 @@
       val avoid_trm' = subst_free (param_trms ~~ prm_trms) avoid_trm 
       val concl_args' = map (subst_free (param_trms ~~ prm_trms)) concl_args 
       
-      val user_thm' = map (cterm_instantiate (intr_cvars ~~ prms)) user_thm
+      val user_thm' = map (infer_instantiate ctxt (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ prms)) user_thm
         |> map (full_simplify (put_simpset HOL_ss ctxt addsimps (@{thm fresh_star_Pair}::prems)))
       
       val fthm = fresh_thm ctxt user_thm' (Thm.term_of p) (Thm.term_of c) concl_args' avoid_trm'
 
       val (([(_, q)], fprop :: fresh_eqs), ctxt') = Obtain.result
-              (K (EVERY1 [etac @{thm exE}, 
+              (K (EVERY1 [eresolve_tac ctxt @{thms exE}, 
                           full_simp_tac (put_simpset HOL_basic_ss ctxt
                             addsimps @{thms supp_Pair fresh_star_Un}),
-                          REPEAT o etac @{thm conjE},
-                          dtac fresh_star_plus,
-                          REPEAT o dtac supp_perm_eq'])) [fthm] ctxt 
+                          REPEAT o eresolve_tac ctxt @{thms conjE},
+                          dresolve_tac ctxt [fresh_star_plus],
+                          REPEAT o dresolve_tac ctxt [supp_perm_eq']])) [fthm] ctxt 
 
       val expand_conv = Conv.try_conv (Conv.rewrs_conv fresh_eqs)
       fun expand_conv_bot ctxt = Conv.bottom_conv (K expand_conv) ctxt
 
-      val cperms = map (Thm.cterm_of ctxt o perm_const) prm_tys
+      val cperms = map (Thm.cterm_of ctxt' o perm_const) prm_tys
       val qp_prms = map2 (fn ct1 => fn ct2 => Thm.mk_binop ct1 (mk_cplus q p) ct2) cperms prms 
       val prem' = prem
-        |> cterm_instantiate (intr_cvars ~~ qp_prms)
-        |> eqvt_srule ctxt
+        |> infer_instantiate ctxt' (map (#1 o dest_Var o Thm.term_of) intr_cvars ~~ qp_prms)
+        |> eqvt_srule ctxt'
 
       val fprop' = eqvt_srule ctxt' fprop 
       val tac_fresh = simp_tac (put_simpset HOL_basic_ss ctxt' addsimps [fprop'])
@@ -268,8 +269,8 @@
 
       (* for non-inductive premises *)   
       fun tac2 prm =  
-        EVERY' [ minus_permute_intro_tac (mk_cplus q p), 
-                 eqvt_stac ctxt, 
+        EVERY' [ minus_permute_intro_tac ctxt' (mk_cplus q p), 
+                 eqvt_stac ctxt', 
                  helper_tac false prm (mk_cplus q p) ctxt' ]
 
       fun select prm (t, i) =
@@ -279,11 +280,11 @@
         (fn {context = ctxt'', ...} => 
            EVERY1 [ CONVERSION (expand_conv_bot ctxt''),
                     eqvt_stac ctxt'',
-                    rtac prem',
+                    resolve_tac ctxt'' [prem'],
                     RANGE (tac_fresh :: map (SUBGOAL o select) prems) ])
         |> singleton (Proof_Context.export ctxt' ctxt)
     in
-      rtac side_thm 1
+      resolve_tac ctxt [side_thm] 1
     end) ctxt
 
 fun case_tac ctxt Ps avoid avoid_trm intr_cvars param_trms prem user_thm concl_args =
@@ -291,17 +292,17 @@
     val tac1 = non_binder_tac prem intr_cvars Ps ctxt
     val tac2 = binder_tac prem intr_cvars param_trms Ps user_thm avoid_trm concl_args ctxt
   in 
-    EVERY' [ rtac @{thm allI}, rtac @{thm allI}, 
+    EVERY' [ resolve_tac ctxt @{thms allI}, resolve_tac ctxt @{thms allI}, 
              if null avoid then tac1 else tac2 ]
   end
 
 fun prove_sinduct_tac raw_induct user_thms Ps avoids avoid_trms intr_cvars param_trms concl_args 
-  {prems, context} =
+  {prems, context = ctxt} =
   let
     val cases_tac = 
-      map7 (case_tac context Ps) avoids avoid_trms intr_cvars param_trms prems user_thms concl_args
+      map7 (case_tac ctxt Ps) avoids avoid_trms intr_cvars param_trms prems user_thms concl_args
   in 
-    EVERY1 [ DETERM o rtac raw_induct, RANGE cases_tac ]
+    EVERY1 [ DETERM o resolve_tac ctxt [raw_induct], RANGE cases_tac ]
   end
 
 val normalise = @{lemma "(Q --> (!p c. P p c)) ==> (!!c. Q ==> P (0::perm) c)" by simp}