src/Tools/induct.ML

   val atomize_tac: int -> tactic
   val inner_atomize_tac: int -> tactic
   val rulified_term: thm -> theory * term
   val rulify_tac: int -> tactic
   val internalize: int -> thm -> thm
-  val guess_instance: thm -> int -> thm -> thm Seq.seq
+  val guess_instance: Proof.context -> thm -> int -> thm -> thm Seq.seq
   val cases_tac: Proof.context -> term option list list -> thm option ->
     thm list -> int -> cases_tactic
   val induct_tac: Proof.context -> (string option * term) option list list ->
     (string * typ) list list -> term option list -> thm list option ->
     thm list -> int -> cases_tactic

     val xs = map2 (curry (cert o Var)) (map #1 pairs) (map (#T o Thm.rep_cterm) ts);
   in (map (fn (xi, (S, T)) => (certT (TVar (xi, S)), certT T)) (Vartab.dest iTs), xs ~~ ts) end;
 
 in
 
-fun guess_instance rule i st =
-  let
-    val thy = Thm.theory_of_thm st;
+fun guess_instance ctxt rule i st =
+  let
+    val thy = ProofContext.theory_of ctxt;
     val maxidx = Thm.maxidx_of st;
     val goal = Thm.term_of (Thm.cprem_of st i);  (*exception Subscript*)
     val params = rev (rename_wrt_term goal (Logic.strip_params goal));
   in
     if not (null params) then
       (warning ("Cannot determine rule instantiation due to pending parameter(s): " ^
-        commas_quote (map (Sign.string_of_term thy o Syntax.mark_boundT) params));
+        commas_quote (map (Syntax.string_of_term ctxt o Syntax.mark_boundT) params));
       Seq.single rule)
     else
       let
         val rule' = Thm.incr_indexes (maxidx + 1) rule;
         val concl = Logic.strip_assums_concl goal;

               THEN' fix_tac defs_ctxt
                 (nth concls (j - 1) + more_consumes)
                 (nth_list arbitrary (j - 1))))
           THEN' inner_atomize_tac) j))
         THEN' atomize_tac) i st |> Seq.maps (fn st' =>
-            guess_instance (internalize more_consumes rule) i st'
+            guess_instance ctxt (internalize more_consumes rule) i st'
             |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking))
             |> Seq.maps (fn rule' =>
               CASES (rule_cases rule' cases)
                 (Tactic.rtac rule' i THEN
                   PRIMITIVE (singleton (ProofContext.export defs_ctxt ctxt))) st'))))

   in
     SUBGOAL_CASES (fn (goal, i) => fn st =>
       ruleq goal
       |> Seq.maps (RuleCases.consume [] facts)
       |> Seq.maps (fn ((cases, (_, more_facts)), rule) =>
-        guess_instance rule i st
+        guess_instance ctxt rule i st
         |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking))
         |> Seq.maps (fn rule' =>
           CASES (RuleCases.make_common false (thy, Thm.prop_of rule') cases)
             (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
   end;