src/Pure/Syntax/syntax_trans.ML

--- a/src/Pure/Syntax/syntax_trans.ML	Thu Jun 09 17:46:25 2011 +0200
+++ b/src/Pure/Syntax/syntax_trans.ML	Thu Jun 09 17:51:49 2011 +0200
@@ -439,7 +439,7 @@
 (* dependent / nondependent quantifiers *)
 
 fun var_abs mark (x, T, b) =
-  let val ([x'], _) = Name.variants [x] (Term.declare_term_names b Name.context)
+  let val (x', _) = Name.variant x (Term.declare_term_names b Name.context)
   in (x', subst_bound (mark (x', T), b)) end;
 
 val variant_abs = var_abs Free;