variants: special treatment of empty name;
authorwenzelm
Wed, 12 Jul 2006 00:34:54 +0200
changeset 20104 f8e7c71926e4
parent 20103 26747ea32d35
child 20105 454f4be984b7
variants: special treatment of empty name;
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