src/Pure/proofterm.ML
changeset 20071 8f3e1ddb50e6
parent 20000 2fa767ab91aa
child 20147 7aa076a45cb4
     1.1 --- a/src/Pure/proofterm.ML	Tue Jul 11 12:16:52 2006 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Tue Jul 11 12:16:54 2006 +0200
     1.3 @@ -568,8 +568,8 @@
     1.4              (([], [], [], []), prf);
     1.5      val fs' = map (fst o dest_Free) fs;
     1.6      val vs' = map (fst o dest_Var) vs;
     1.7 -    val names = vs' ~~ variantlist (map fst vs', fs');
     1.8 -    val names' = Tvs ~~ variantlist (map fst Tvs, Tfs);
     1.9 +    val names = vs' ~~ Name.variant_list fs' (map fst vs');
    1.10 +    val names' = Tvs ~~ Name.variant_list Tfs (map fst Tvs);
    1.11      val rnames = map swap names;
    1.12      val rnames' = map swap names';
    1.13    in
    1.14 @@ -607,7 +607,7 @@
    1.15      val fs = Term.fold_types (Term.fold_atyps
    1.16        (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
    1.17      val ixns = add_term_tvar_ixns (t, []);
    1.18 -    val fmap = fs ~~ variantlist (map fst fs, map #1 ixns)
    1.19 +    val fmap = fs ~~ Name.variant_list (map #1 ixns) (map fst fs)
    1.20      fun thaw (f as (a, S)) =
    1.21        (case AList.lookup (op =) fmap f of
    1.22          NONE => TFree f
    1.23 @@ -619,7 +619,7 @@
    1.24  local
    1.25  
    1.26  fun new_name (ix, (pairs,used)) =
    1.27 -  let val v = variant used (string_of_indexname ix)
    1.28 +  let val v = Name.variant used (string_of_indexname ix)
    1.29    in  ((ix, v) :: pairs, v :: used)  end;
    1.30  
    1.31  fun freeze_one alist (ix, sort) = (case AList.lookup (op =) alist ix of