src/Pure/name.ML
changeset 20104 f8e7c71926e4
parent 20099 bc3f9cb33645
child 20121 848fc1a1d355
equal deleted inserted replaced
20103:26747ea32d35 20104:f8e7c71926e4
   108     fun vary x =
   108     fun vary x =
   109       (case declared ctxt x of
   109       (case declared ctxt x of
   110         NONE => x
   110         NONE => x
   111       | SOME x' => vary (Symbol.bump_string (the_default x x')));
   111       | SOME x' => vary (Symbol.bump_string (the_default x x')));
   112 
   112 
   113     val (x, n) = clean_index (name, 0);
   113     val (raw_x, n) = clean_index (name, 0);
       
   114     val x = if raw_x = "" then "u" else raw_x;
   114     val (x', ctxt') =
   115     val (x', ctxt') =
   115       if is_none (declared ctxt x) then (x, declare x ctxt)
   116       if is_none (declared ctxt x) then (x, declare x ctxt)
   116       else
   117       else
   117         let
   118         let
   118           val x0 = Symbol.bump_init x;
   119           val x0 = Symbol.bump_init x;