# HG changeset patch
# User wenzelm
# Date 1152657294 -7200
# Node ID f8e7c71926e4bca1f025c0f21dee430860bb3f43
# Parent  26747ea32d35e339ce1b4fc3d8e4d06268e412c8
variants: special treatment of empty name;

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