diff -r 26747ea32d35 -r f8e7c71926e4 src/Pure/name.ML --- a/src/Pure/name.ML Tue Jul 11 23:49:32 2006 +0200 +++ b/src/Pure/name.ML Wed Jul 12 00:34:54 2006 +0200 @@ -110,7 +110,8 @@ NONE => x | SOME x' => vary (Symbol.bump_string (the_default x x'))); - val (x, n) = clean_index (name, 0); + val (raw_x, n) = clean_index (name, 0); + val x = if raw_x = "" then "u" else raw_x; val (x', ctxt') = if is_none (declared ctxt x) then (x, declare x ctxt) else