diff -r 5ec55c1fa116 -r e063c0403650 src/Pure/term.ML
--- a/src/Pure/term.ML	Sun Sep 25 20:24:23 2005 +0200
+++ b/src/Pure/term.ML	Sun Sep 25 23:36:14 2005 +0200
@@ -1262,7 +1262,7 @@
 fun zero_var_inst vars =
   fold (fn v as ((x, i), X) => fn (used, inst) =>
     let
-      val x' = variant used x;
+      val x' = variant used (if is_bound x then "u" else x);
       val used' = x' :: used;
     in if x = x' andalso i = 0 then (used', inst) else (used', (v, ((x', 0), X)) :: inst) end)
   vars ([], []) |> #2;