src/Pure/variable.ML
changeset 33037 b22e44496dc2
parent 32784 1a5dde5079ac
child 33038 8f9594c31de4
     1.1 --- a/src/Pure/variable.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/Pure/variable.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -301,7 +301,7 @@
     1.4      val names = names_of ctxt;
     1.5      val (xs', names') =
     1.6        if is_body ctxt then Name.variants xs names |>> map Name.skolem
     1.7 -      else (no_dups (xs inter_string ys); no_dups (xs inter_string zs);
     1.8 +      else (no_dups (gen_inter (op =) (xs, ys)); no_dups (gen_inter (op =) (xs, zs));
     1.9          (xs, fold Name.declare xs names));
    1.10    in ctxt |> new_fixes names' xs xs' end;
    1.11