eliminated qualified_names naming policy: qualified names are only permitted via explicit Binding.qualify/qualified_name etc. (NB: user-level outer syntax should never do this);

--- 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

--- a/src/Pure/Isar/element.ML	Wed Mar 11 15:45:40 2009 +0100
+++ b/src/Pure/Isar/element.ML	Wed Mar 11 16:36:27 2009 +0100
@@ -518,8 +518,8 @@
     fun activate elem ctxt =
       let val elem' = (map_ctxt_attrib Args.assignable o prep_facts ctxt) elem
       in (elem', activate_elem elem' ctxt) end
-    val (elems, ctxt') = fold_map activate raw_elems (ProofContext.qualified_names ctxt);
-  in (elems |> map (map_ctxt_attrib Args.closure), ProofContext.restore_naming ctxt ctxt') end;
+    val (elems, ctxt') = fold_map activate raw_elems ctxt;
+  in (elems |> map (map_ctxt_attrib Args.closure), ctxt') end;
 
 fun check_name name =
   if Long_Name.is_qualified name then error ("Illegal qualified name: " ^ quote name)

--- a/src/Pure/Isar/local_theory.ML	Wed Mar 11 15:45:40 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML	Wed Mar 11 16:36:27 2009 +0100
@@ -138,14 +138,12 @@
 
 fun full_naming lthy =
   Sign.naming_of (ProofContext.theory_of lthy)
-  |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy))
-  |> NameSpace.qualified_names;
+  |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy));
 
 fun full_name naming = NameSpace.full_name (full_naming naming);
 
 fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
   |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy))
-  |> Sign.qualified_names
   |> f
   ||> Sign.restore_naming thy);
 

--- a/src/Pure/Isar/locale.ML	Wed Mar 11 15:45:40 2009 +0100
+++ b/src/Pure/Isar/locale.ML	Wed Mar 11 16:36:27 2009 +0100
@@ -107,19 +107,6 @@
 
 datatype ctxt = datatype Element.ctxt;
 
-fun global_note_qualified kind facts thy = (*FIXME*)
-  thy
-  |> Sign.qualified_names
-  |> PureThy.note_thmss kind facts
-  ||> Sign.restore_naming thy;
-
-fun local_note_qualified kind facts ctxt = (*FIXME*)
-  ctxt
-  |> ProofContext.qualified_names
-  |> ProofContext.note_thmss_i kind facts
-  ||> ProofContext.restore_naming ctxt;
-
-
 
 (*** Theory data ***)
 
@@ -337,7 +324,7 @@
 fun init_global_elem (Notes (kind, facts)) thy =
   let
     val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
-  in global_note_qualified kind facts' thy |> snd end
+  in PureThy.note_thmss kind facts' thy |> snd end
 
 fun init_local_elem (Fixes fixes) ctxt = ctxt |>
       ProofContext.add_fixes_i fixes |> snd
@@ -359,7 +346,7 @@
   | init_local_elem (Notes (kind, facts)) ctxt =
       let
         val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
-      in local_note_qualified kind facts' ctxt |> snd end
+      in ProofContext.note_thmss_i kind facts' ctxt |> snd end
 
 fun cons_elem false (Notes notes) elems = elems
   | cons_elem _ elem elems = elem :: elems
@@ -452,7 +439,7 @@
             let
               val args'' = snd args' |> Element.facts_map (Element.morph_ctxt morph) |>
                 Attrib.map_facts (Attrib.attribute_i thy)
-            in global_note_qualified kind args'' #> snd end)
+            in PureThy.note_thmss kind args'' #> snd end)
         (get_registrations thy |> filter (fn (name, _) => name = loc)) thy))
   in ctxt'' end;
 

--- a/src/Pure/Isar/proof_context.ML	Wed Mar 11 15:45:40 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Wed Mar 11 16:36:27 2009 +0100
@@ -98,7 +98,6 @@
   val get_thm: Proof.context -> xstring -> thm
   val add_path: string -> Proof.context -> Proof.context
   val sticky_prefix: string -> Proof.context -> Proof.context
-  val qualified_names: Proof.context -> Proof.context
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val reset_naming: Proof.context -> Proof.context
   val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
@@ -947,7 +946,6 @@
 
 val add_path        = map_naming o NameSpace.add_path;
 val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
-val qualified_names = map_naming NameSpace.qualified_names;
 val restore_naming  = map_naming o K o naming_of;
 val reset_naming    = map_naming (K local_naming);
 

--- a/src/Pure/Isar/theory_target.ML	Wed Mar 11 15:45:40 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Wed Mar 11 16:36:27 2009 +0100
@@ -144,12 +144,6 @@
 
   in (result'', result) end;
 
-fun note_local kind facts ctxt =
-  ctxt
-  |> ProofContext.qualified_names
-  |> ProofContext.note_thmss_i kind facts
-  ||> ProofContext.restore_naming ctxt;
-
 fun notes (Target {target, is_locale, ...}) kind facts lthy =
   let
     val thy = ProofContext.theory_of lthy;
@@ -165,12 +159,10 @@
       |> Attrib.map_facts (if is_locale then K I else Attrib.attribute_i thy);
   in
     lthy |> LocalTheory.theory
-      (Sign.qualified_names
-        #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
-        #> Sign.restore_naming thy)
-    |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
+      (PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd)
+    |> not is_locale ? LocalTheory.target (ProofContext.note_thmss_i kind global_facts #> snd)
     |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
-    |> note_local kind local_facts
+    |> ProofContext.note_thmss_i kind local_facts
   end;
 
 

--- a/src/Pure/sign.ML	Wed Mar 11 15:45:40 2009 +0100
+++ b/src/Pure/sign.ML	Wed Mar 11 16:36:27 2009 +0100
@@ -126,7 +126,6 @@
   val parent_path: theory -> theory
   val sticky_prefix: string -> theory -> theory
   val no_base_names: theory -> theory
-  val qualified_names: theory -> theory
   val local_path: theory -> theory
   val restore_naming: theory -> theory -> theory
   val hide_class: bool -> string -> theory -> theory
@@ -622,7 +621,6 @@
 val parent_path     = map_naming NameSpace.parent_path;
 val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
 val no_base_names   = map_naming NameSpace.no_base_names;
-val qualified_names = map_naming NameSpace.qualified_names;
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);