author | wenzelm |
Wed, 12 Jul 2006 00:34:54 +0200 | |
changeset 20104 | f8e7c71926e4 |
parent 20103 | 26747ea32d35 |
child 20105 | 454f4be984b7 |
src/Pure/name.ML | file | annotate | diff | comparison | revisions |
--- 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