src/Pure/term.ML

--- a/src/Pure/term.ML	Thu Jun 09 15:38:49 2011 +0200
+++ b/src/Pure/term.ML	Thu Jun 09 16:34:49 2011 +0200
@@ -936,7 +936,8 @@
       | name_clash (Abs (_, _, t)) = name_clash t
       | name_clash _ = false;
   in
-    if name_clash body then dest_abs (Name.variant [x] x, T, body)    (*potentially slow*)
+    if name_clash body then
+      dest_abs (singleton (Name.variant_list [x]) x, T, body)    (*potentially slow*)
     else (x, subst_bound (Free (x, T), body))
   end;