--- a/src/Pure/codegen.ML Wed Oct 21 12:02:19 2009 +0200
+++ b/src/Pure/codegen.ML Wed Oct 21 12:02:56 2009 +0200
@@ -599,8 +599,8 @@
else Pretty.block (separate (Pretty.brk 1) (p :: ps));
fun new_names t xs = Name.variant_list
- (union (op =) (map (fst o fst o dest_Var) (OldTerm.term_vars t),
- OldTerm.add_term_names (t, ML_Syntax.reserved_names))) (map mk_id xs);
+ (union (op =) (map (fst o fst o dest_Var) (OldTerm.term_vars t))
+ (OldTerm.add_term_names (t, ML_Syntax.reserved_names))) (map mk_id xs);
fun new_name t x = hd (new_names t [x]);