src/HOL/Tools/Old_Datatype/old_datatype_aux.ML

   val mk_conj : term list -> term
   val mk_disj : term list -> term
 
   val app_bnds : term -> int -> term
 
-  val ind_tac : thm -> string list -> int -> tactic
+  val ind_tac : Proof.context -> thm -> string list -> int -> tactic
   val exh_tac : Proof.context -> (string -> thm) -> int -> tactic
 
   exception Datatype
   exception Datatype_Empty of string
   val name_of_typ : typ -> string

 fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
 
 
 (* instantiate induction rule *)
 
-fun ind_tac indrule indnames = CSUBGOAL (fn (cgoal, i) =>
-  let
-    val thy = Thm.theory_of_cterm cgoal;
+fun ind_tac ctxt indrule indnames = CSUBGOAL (fn (cgoal, i) =>
+  let
     val goal = Thm.term_of cgoal;
     val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of indrule));
     val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop (Logic.strip_imp_concl goal));
     val getP =
       if can HOLogic.dest_imp (hd ts)

           (case flt (Term.add_frees t2 []) of
             [(s, T)] => SOME (absfree (s, T) t2)
           | _ => NONE)
       | SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2))));
     val insts =
-      map_filter (fn (t, u) =>
+      (ts ~~ ts') |> map_filter (fn (t, u) =>
         (case abstr (getP u) of
           NONE => NONE
-        | SOME u' =>
-            SOME (apply2 (Thm.global_cterm_of thy) (t |> getP |> snd |> head_of, u')))) (ts ~~ ts');
+        | SOME u' => SOME (apply2 (Thm.cterm_of ctxt) (t |> getP |> snd |> head_of, u'))));
     val indrule' = cterm_instantiate insts indrule;
   in resolve0_tac [indrule'] i end);
 
 
 (* perform exhaustive case analysis on last parameter of subgoal i *)