src/Pure/General/name_space.ML

--- a/src/Pure/General/name_space.ML	Wed Mar 11 15:45:40 2009 +0100
+++ b/src/Pure/General/name_space.ML	Wed Mar 11 16:36:27 2009 +0100
@@ -36,7 +36,6 @@
   val root_path: naming -> naming
   val parent_path: naming -> naming
   val no_base_names: naming -> naming
-  val qualified_names: naming -> naming
   val sticky_prefix: string -> naming -> naming
   type 'a table = T * 'a Symtab.table
   val bind: naming -> binding * 'a -> 'a table -> string * 'a table       (*exception Symtab.DUP*)
@@ -174,53 +173,44 @@
 
 datatype naming = Naming of
  {path: (string * bool) list,
-  no_base_names: bool,
-  qualified_names: bool};
+  no_base_names: bool};
 
-fun make_naming (path, no_base_names, qualified_names) =
-  Naming {path = path, no_base_names = no_base_names, qualified_names = qualified_names};
+fun make_naming (path, no_base_names) =
+  Naming {path = path, no_base_names = no_base_names};
 
-fun map_naming f (Naming {path, no_base_names, qualified_names}) =
-  make_naming (f (path, no_base_names, qualified_names));
-
-fun path_of (Naming {path, ...}) = path;
+fun map_naming f (Naming {path, no_base_names}) =
+  make_naming (f (path, no_base_names));
 
 
 (* configure naming *)
 
-val default_naming = make_naming ([], false, false);
+val default_naming = make_naming ([], false);
 
-fun add_path elems = map_naming (fn (path, no_base_names, qualified_names) =>
-  (path @ map (rpair false) (Long_Name.explode elems), no_base_names, qualified_names));
+fun add_path elems = map_naming (fn (path, no_base_names) =>
+  (path @ map (rpair false) (Long_Name.explode elems), no_base_names));
 
-val root_path = map_naming (fn (_, no_base_names, qualified_names) =>
-  ([], no_base_names, qualified_names));
+val root_path = map_naming (fn (_, no_base_names) => ([], no_base_names));
 
-val parent_path = map_naming (fn (path, no_base_names, qualified_names) =>
-  (perhaps (try (#1 o split_last)) path, no_base_names, qualified_names));
+val parent_path = map_naming (fn (path, no_base_names) =>
+  (perhaps (try (#1 o split_last)) path, no_base_names));
 
-fun sticky_prefix elems = map_naming (fn (path, no_base_names, qualified_names) =>
-  (path @ map (rpair true) (Long_Name.explode elems), no_base_names, qualified_names));
+fun sticky_prefix elems = map_naming (fn (path, no_base_names) =>
+  (path @ map (rpair true) (Long_Name.explode elems), no_base_names));
 
-val no_base_names = map_naming (fn (path, _, qualified_names) => (path, true, qualified_names));
-val qualified_names = map_naming (fn (path, no_base_names, _) => (path, no_base_names, true));
+val no_base_names = map_naming (fn (path, _) => (path, true));
 
 
 (* full name *)
 
 fun err_bad binding = error ("Bad name declaration " ^ quote (Binding.str_of binding));
 
-fun name_spec (Naming {path, qualified_names, ...}) binding =
+fun name_spec (Naming {path, ...}) binding =
   let
     val (prefix, name) = Binding.dest binding;
-    val _ = not qualified_names andalso Long_Name.is_qualified name andalso err_bad binding;
+    val _ = Long_Name.is_qualified name andalso err_bad binding;
 
     val spec1 = maps (fn (a, b) => map (rpair b) (Long_Name.explode a)) (path @ prefix);
-    val spec2 =
-      (case try split_last (Long_Name.explode name) of
-        NONE => []
-      | SOME (qual, base) => map (rpair false) qual @ [(base, true)]);
-
+    val spec2 = if name = "" then [] else [(name, true)];
     val spec = spec1 @ spec2;
     val _ =
       exists (fn (a, _) => a = "" orelse a = "??" orelse exists_string (fn s => s = "\"") a) spec