src/Tools/induct.ML

           let
             val cx = cert x;
             val {T = xT, thy, ...} = Thm.rep_cterm cx;
             val ct = cert (tune t);
           in
-            if Sign.typ_instance thy (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct)
+            if Type.could_unify (#T (Thm.rep_cterm ct), xT) then SOME (cx, ct)
             else error (Pretty.string_of (Pretty.block
              [Pretty.str "Ill-typed instantiation:", Pretty.fbrk,
               Display.pretty_cterm ct, Pretty.str " ::", Pretty.brk 1,
               Display.pretty_ctyp (#T (Thm.crep_cterm ct))]))
           end

                 (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'
-            |> Seq.map (rule_instance thy taking)
+            |> 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'))))
     THEN_ALL_NEW_CASES rulify_tac

     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
-        |> Seq.map (rule_instance thy taking)
+        |> Seq.map (rule_instance thy (burrow_options (Variable.polymorphic ctxt) taking))
         |> Seq.maps (fn rule' =>
           CASES (make_cases is_open rule' cases)
             (Method.insert_tac more_facts i THEN Tactic.rtac rule' i) st)))
   end;