src/Pure/codegen.ML
changeset 33037 b22e44496dc2
parent 33001 82382652e5e7
child 33038 8f9594c31de4
     1.1 --- a/src/Pure/codegen.ML	Tue Oct 20 13:37:56 2009 +0200
     1.2 +++ b/src/Pure/codegen.ML	Tue Oct 20 16:13:01 2009 +0200
     1.3 @@ -599,8 +599,8 @@
     1.4       else Pretty.block (separate (Pretty.brk 1) (p :: ps));
     1.5  
     1.6  fun new_names t xs = Name.variant_list
     1.7 -  (map (fst o fst o dest_Var) (OldTerm.term_vars t) union
     1.8 -    OldTerm.add_term_names (t, ML_Syntax.reserved_names)) (map mk_id xs);
     1.9 +  (gen_union (op =) (map (fst o fst o dest_Var) (OldTerm.term_vars t),
    1.10 +    OldTerm.add_term_names (t, ML_Syntax.reserved_names))) (map mk_id xs);
    1.11  
    1.12  fun new_name t x = hd (new_names t [x]);
    1.13