1.1 --- a/src/Pure/variable.ML	Thu Jun 09 17:46:25 2011 +0200
     1.2 +++ b/src/Pure/variable.ML	Thu Jun 09 17:51:49 2011 +0200
     1.3 @@ -255,7 +255,7 @@
     1.4  fun variant_frees ctxt ts frees =
     1.5    let
     1.6      val names = names_of (fold declare_names ts ctxt);
     1.7 -    val xs = fst (Name.variants (map #1 frees) names);
     1.8 +    val xs = fst (fold_map Name.variant (map #1 frees) names);
     1.9    in xs ~~ map snd frees end;
    1.10  
    1.11  
    1.12 @@ -365,7 +365,7 @@
    1.13      val xs = map check_name bs;
    1.14      val names = names_of ctxt;
    1.15      val (xs', names') =
    1.16 -      if is_body ctxt then Name.variants xs names |>> map Name.skolem
    1.17 +      if is_body ctxt then fold_map Name.variant xs names |>> map Name.skolem
    1.18        else (xs, fold Name.declare xs names);
    1.19    in ctxt |> new_fixes names' xs xs' (map Binding.pos_of bs) end;
    1.20  
    1.21 @@ -373,7 +373,7 @@
    1.22    let
    1.23      val names = names_of ctxt;
    1.24      val xs = map (fn x => Name.clean x |> can Name.dest_internal x ? Name.internal) raw_xs;
    1.25 -    val (xs', names') = Name.variants xs names |>> (is_body ctxt ? map Name.skolem);
    1.26 +    val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem);
    1.27    in ctxt |> new_fixes names' xs xs' (replicate (length xs) Position.none) end;
    1.28  
    1.29  end;