1.1 --- a/src/Pure/Isar/obtain.ML	Tue Jul 11 12:17:09 2006 +0200
     1.2 +++ b/src/Pure/Isar/obtain.ML	Tue Jul 11 12:17:11 2006 +0200
     1.3 @@ -120,7 +120,7 @@
     1.4      val _ = Variable.warn_extra_tfrees fix_ctxt asms_ctxt;
     1.5  
     1.6      (*obtain statements*)
     1.7 -    val thesisN = Term.variant xs AutoBind.thesisN;
     1.8 +    val thesisN = Name.variant xs AutoBind.thesisN;
     1.9      val (thesis_var, thesis) = bind_judgment fix_ctxt thesisN;
    1.10  
    1.11      fun occs_var x = Library.get_first (fn t =>
    1.12 @@ -196,7 +196,7 @@
    1.13  
    1.14      val xs = map (apsnd norm_type o fst) vars;
    1.15      val ys = map (apsnd norm_type) (Library.drop (m, params));
    1.16 -    val ys' = map Term.internal (Term.variantlist (map fst ys, map fst xs)) ~~ map #2 ys;
    1.17 +    val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys;
    1.18      val terms = map (Drule.mk_term o cert o Free) (xs @ ys');
    1.19  
    1.20      val instT =