# HG changeset patch
# User wenzelm
# Date 1152790917 -7200
# Node ID 848fc1a1d3552f9fa421331678a67bbe454d8e70
# Parent  4fcabd21e2aa1c8796212a6ce43af3f5b7b0bf83
do not export make_context;
initial context: declare empty names;
variants: no special treatment of empty names;

diff -r 4fcabd21e2aa -r 848fc1a1d355 src/Pure/name.ML
--- a/src/Pure/name.ML	Thu Jul 13 13:41:53 2006 +0200
+++ b/src/Pure/name.ML	Thu Jul 13 13:41:57 2006 +0200
@@ -17,7 +17,6 @@
   val clean: string -> string
   type context
   val context: context
-  val make_context: string list -> context
   val declare: string -> context -> context
   val invents: context -> string -> int -> string list
   val invent_list: string list -> string -> int -> string list
@@ -80,7 +79,7 @@
 
 fun declared (Context tab) = Symtab.lookup tab;
 
-val context = Context Symtab.empty;
+val context = Context Symtab.empty |> fold declare ["", "'"];
 fun make_context used = fold declare used context;
 
 
@@ -110,8 +109,7 @@
         NONE => x
       | SOME x' => vary (Symbol.bump_string (the_default x x')));
 
-    val (raw_x, n) = clean_index (name, 0);
-    val x = if raw_x = "" then "u" else raw_x;
+    val (x, n) = clean_index (name, 0);
     val (x', ctxt') =
       if is_none (declared ctxt x) then (x, declare x ctxt)
       else