src/Pure/Isar/obtain.ML

 
 val mk_all_external = Logic.all_constraint o Variable.default_type;
 
 fun mk_all_internal ctxt (y, z) t =
   let
+    val frees =
+      (t, Term_Subst.Frees.empty)
+      |-> Term.fold_aterms (fn Free v => Term_Subst.Frees.add (v, ()) | _ => I);
     val T =
-      (case AList.lookup (op =) (Term.add_frees t []) z of
+      (case Term_Subst.Frees.get_first (fn ((x, T), ()) => if x = z then SOME T else NONE) frees of
         SOME T => T
       | NONE => the_default dummyT (Variable.default_type ctxt z));
   in Logic.all_const T $ Term.lambda_name (y, Free (z, T)) t end;
 
 fun prepare_clause prep_var parse_prop mk_all ctxt thesis raw_vars raw_props =

     val ys = map (apsnd norm_type) (drop m params);
     val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys;
     val terms = map (Drule.mk_term o Thm.cterm_of ctxt o Free) (xs @ ys');
 
     val instT =
-      fold (Term.add_tvarsT o #2) params []
-      |> map (fn v => (v, Thm.ctyp_of ctxt (norm_type (TVar v))));
+      (params, Term_Subst.TVars.empty) |-> fold (#2 #> Term.fold_atyps (fn T => fn instT =>
+        (case T of
+          TVar v =>
+            if Term_Subst.TVars.defined instT v then instT
+            else Term_Subst.TVars.update (v, Thm.ctyp_of ctxt (norm_type T)) instT
+        | _ => instT)));
     val closed_rule = rule
       |> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var))
-      |> Thm.instantiate (instT, []);
+      |> Thm.instantiate (Term_Subst.TVars.dest instT, []);
 
     val ((_, rule' :: terms'), ctxt') = Variable.import false (closed_rule :: terms) ctxt;
     val vars' =
       map (dest_Free o Thm.term_of o Drule.dest_term) terms' ~~
       (map snd vars @ replicate (length ys) NoSyn);