# HG changeset patch
# User wenzelm
# Date 1236986030 -3600
# Node ID e26b806471897b5e849529cdf884ea268017687b
# Parent  3ec2d35b380fdd074969c66327ecd03adcf3efcc
removed obsolete no_base_names naming policy;

diff -r 3ec2d35b380f -r e26b80647189 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Fri Mar 13 23:56:07 2009 +0100
+++ b/src/Pure/General/name_space.ML	Sat Mar 14 00:13:50 2009 +0100
@@ -35,7 +35,6 @@
   val add_path: string -> naming -> naming
   val root_path: naming -> naming
   val parent_path: naming -> naming
-  val no_base_names: naming -> naming
   val mandatory_path: string -> naming -> naming
   type 'a table = T * 'a Symtab.table
   val define: naming -> binding * 'a -> 'a table -> string * 'a table (*exception Symtab.DUP*)
@@ -171,40 +170,22 @@
 
 (* datatype naming *)
 
-datatype naming = Naming of
- {path: (string * bool) list,
-  no_base_names: bool};
+datatype naming = Naming of (string * bool) list;
+fun map_naming f (Naming path) = Naming (f path);
 
-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}) =
-  make_naming (f (path, no_base_names));
-
-
-(* configure naming *)
+val default_naming = Naming [];
 
-val default_naming = make_naming ([], false);
-
-fun add_path elems = map_naming (fn (path, no_base_names) =>
-  (path @ [(elems, false)], no_base_names));
-
-val root_path = map_naming (fn (_, no_base_names) => ([], no_base_names));
-
-val parent_path = map_naming (fn (path, no_base_names) =>
-  (perhaps (try (#1 o split_last)) path, no_base_names));
-
-fun mandatory_path elems = map_naming (fn (path, no_base_names) =>
-  (path @ [(elems, true)], no_base_names));
-
-val no_base_names = map_naming (fn (path, _) => (path, true));
+fun add_path elems = map_naming (fn path => path @ [(elems, false)]);
+val root_path = map_naming (fn _ => []);
+val parent_path = map_naming (perhaps (try (#1 o split_last)));
+fun mandatory_path elems = map_naming (fn path => path @ [(elems, true)]);
 
 
 (* full name *)
 
 fun err_bad binding = error ("Bad name binding " ^ quote (Binding.str_of binding));
 
-fun name_spec (Naming {path, ...}) binding =
+fun name_spec (Naming path) binding =
   let
     val (prefix, name) = Binding.dest binding;
     val _ = Long_Name.is_qualified name andalso err_bad binding;
@@ -232,16 +213,12 @@
 
 fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
 
-fun accesses (naming as Naming {no_base_names, ...}) binding =
+fun accesses naming binding =
   let
     val spec = name_spec naming binding;
     val sfxs = mandatory_suffixes spec;
     val pfxs = mandatory_prefixes spec;
-  in
-    (sfxs @ pfxs, sfxs)
-    |> pairself (no_base_names ? filter (fn [_] => false | _ => true))
-    |> pairself (map Long_Name.implode)
-  end;
+  in pairself (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;
 
 fun external_names naming = #2 o accesses naming o Binding.qualified_name;
 
diff -r 3ec2d35b380f -r e26b80647189 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Mar 13 23:56:07 2009 +0100
+++ b/src/Pure/sign.ML	Sat Mar 14 00:13:50 2009 +0100
@@ -125,7 +125,6 @@
   val root_path: theory -> theory
   val parent_path: theory -> theory
   val mandatory_path: string -> theory -> theory
-  val no_base_names: theory -> theory
   val local_path: theory -> theory
   val restore_naming: theory -> theory -> theory
   val hide_class: bool -> string -> theory -> theory
@@ -616,15 +615,14 @@
 
 (* naming *)
 
-val add_path        = map_naming o NameSpace.add_path;
-val root_path       = map_naming NameSpace.root_path;
-val parent_path     = map_naming NameSpace.parent_path;
-val mandatory_path  = map_naming o NameSpace.mandatory_path;
-val no_base_names   = map_naming NameSpace.no_base_names;
+val add_path = map_naming o NameSpace.add_path;
+val root_path = map_naming NameSpace.root_path;
+val parent_path = map_naming NameSpace.parent_path;
+val mandatory_path = map_naming o NameSpace.mandatory_path;
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
 
-val restore_naming  = map_naming o K o naming_of;
+val restore_naming = map_naming o K o naming_of;
 
 
 (* hide names *)