--- a/Nominal/nominal_induct.ML	Mon Jul 20 11:21:59 2015 +0100
+++ b/Nominal/nominal_induct.ML	Sat Mar 19 21:06:48 2016 +0000
@@ -5,9 +5,8 @@
 
 structure NominalInduct:
 sig
-  val nominal_induct_tac: Proof.context -> bool -> (binding option * (term * bool)) option list list ->
-    (string * typ) list -> (string * typ) list list -> thm list -> thm list -> int -> Rule_Cases.cases_tactic
-
+  val nominal_induct_tac: bool -> (binding option * (term * bool)) option list list ->
+    (string * typ) list -> (string * typ) list list -> thm list -> thm list -> int -> context_tactic
   val nominal_induct_method: (Proof.context -> Proof.method) context_parser
 end =
 
@@ -19,7 +18,7 @@
 fun tuple ts = HOLogic.unit |> fold (fn t => fn u => HOLogic.mk_prod (u, t)) ts;
 
 fun tuple_fun Ts (xi, T) =
-  Library.funpow (length Ts) HOLogic.mk_split
+  Library.funpow (length Ts) HOLogic.mk_case_prod
     (Var (xi, (HOLogic.unitT :: Ts) ---> Term.range_type T));
 
 fun split_all_tuples ctxt =
@@ -57,9 +56,9 @@
       end;
      val substs =
        map2 subst insts concls |> flat |> distinct (op =)
-       |> map (apply2 (Thm.cterm_of ctxt));
+       |> map (fn (t, u) => (#1 (dest_Var t), Thm.cterm_of ctxt u));
   in 
-    (((cases, nconcls), consumes), Drule.cterm_instantiate substs joined_rule) 
+    (((cases, nconcls), consumes), infer_instantiate ctxt substs joined_rule) 
   end;
 
 fun rename_params_rule internal xs rule =
@@ -79,12 +78,12 @@
     fun rename_prems prop =
       let val (As, C) = Logic.strip_horn prop
       in Logic.list_implies (map rename As, C) end;
-  in Thm.equal_elim (Thm.reflexive (Drule.cterm_fun rename_prems (Thm.cprop_of rule))) rule end;
+  in Thm.renamed_prop (rename_prems (Thm.prop_of rule)) rule end;
 
 
 (* nominal_induct_tac *)
 
-fun nominal_induct_tac ctxt simp def_insts avoiding fixings rules facts =
+fun nominal_induct_tac simp def_insts avoiding fixings rules facts i (ctxt, st) =
   let
     val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list;
     val atomized_defs = map (map (Conv.fconv_rule (Induct.atomize_cterm defs_ctxt))) defs;
@@ -97,8 +96,8 @@
     fun rule_cases ctxt r =
       let val r' = if simp then Induct.simplified_rule ctxt r else r
       in Rule_Cases.make_nested ctxt (Thm.prop_of r') (Induct.rulified_term ctxt r') end;
-  in
-    (fn i => fn st =>
+
+    fun context_tac _ _ =
       rules
       |> inst_mutual_rule ctxt insts avoiding
       |> Rule_Cases.consume ctxt (flat defs) facts
@@ -111,7 +110,7 @@
               val xs = nth_list fixings (j - 1);
               val k = nth concls (j - 1) + more_consumes
             in
-              Method.insert_tac (more_facts @ adefs) THEN'
+              Method.insert_tac ctxt (more_facts @ adefs) THEN'
                 (if simp then
                    Induct.rotate_tac k (length adefs) THEN'
                    Induct.arbitrary_tac defs_ctxt k
@@ -124,13 +123,15 @@
             Induct.guess_instance ctxt
               (finish_rule (Induct.internalize ctxt more_consumes rule)) i st'
             |> Seq.maps (fn rule' =>
-              CASES (rule_cases ctxt rule' cases)
-                (Tactic.rtac (rename_params_rule false [] rule') i THEN
-                  PRIMITIVE (singleton (Proof_Context.export defs_ctxt ctxt))) st'))))
-    THEN_ALL_NEW_CASES
+              CONTEXT_CASES (rule_cases ctxt rule' cases)
+                (resolve_tac ctxt [rename_params_rule false [] rule'] i THEN
+                  PRIMITIVE
+                    (singleton (Proof_Context.export defs_ctxt
+                      (Proof_Context.transfer (Proof_Context.theory_of defs_ctxt) ctxt)))) (ctxt, st'))));
+  in
+    (context_tac CONTEXT_THEN_ALL_NEW
       ((if simp then Induct.simplify_tac ctxt THEN' (TRY o Induct.trivial_tac ctxt)
-        else K all_tac)
-       THEN_ALL_NEW Induct.rulify_tac ctxt)
+        else K all_tac) THEN_ALL_NEW Induct.rulify_tac ctxt)) i (ctxt, st)
   end;
 
 
@@ -173,8 +174,8 @@
   Scan.lift (Args.mode Induct.no_simpN) -- 
     (Parse.and_list' (Scan.repeat (unless_more_args def_inst)) --
       avoiding -- fixing -- rule_spec) >>
-  (fn (no_simp, (((x, y), z), w)) => fn ctxt => fn facts =>
-    HEADGOAL (nominal_induct_tac ctxt (not no_simp) x y z w facts));
+  (fn (no_simp, (((x, y), z), w)) => fn _ => fn facts =>
+    nominal_induct_tac (not no_simp) x y z w facts 1);
 
 end