src/Pure/Isar/obtain.ML

     val asms = map fst (Attrib.map_specs (prep_att thy) raw_asms) ~~ proppss;
 
     val _ = Variable.warn_extra_tfrees fix_ctxt asms_ctxt;
 
     (*obtain statements*)
-    val thesisN = Term.variant xs AutoBind.thesisN;
+    val thesisN = Name.variant xs AutoBind.thesisN;
     val (thesis_var, thesis) = bind_judgment fix_ctxt thesisN;
 
     fun occs_var x = Library.get_first (fn t =>
       Term.find_free t (ProofContext.get_skolem fix_ctxt x)) asm_props;
     val parms =

       (Vartab.empty, Int.max (maxidx, Thm.maxidx_of rule));
     val norm_type = Envir.norm_type tyenv;
 
     val xs = map (apsnd norm_type o fst) vars;
     val ys = map (apsnd norm_type) (Library.drop (m, params));
-    val ys' = map Term.internal (Term.variantlist (map fst ys, map fst xs)) ~~ map #2 ys;
+    val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys;
     val terms = map (Drule.mk_term o cert o Free) (xs @ ys');
 
     val instT =
       fold (Term.add_tvarsT o #2) params []
       |> map (TVar #> (fn T => (certT T, certT (norm_type T))));