tuned signature;

--- a/src/Doc/Implementation/Prelim.thy	Mon Oct 13 21:57:40 2014 +0200
+++ b/src/Doc/Implementation/Prelim.thy	Mon Oct 13 22:43:29 2014 +0200
@@ -922,7 +922,7 @@
   \end{mldecls}
   \begin{mldecls}
   @{index_ML_type Name_Space.naming} \\
-  @{index_ML Name_Space.default_naming: Name_Space.naming} \\
+  @{index_ML Name_Space.global_naming: Name_Space.naming} \\
   @{index_ML Name_Space.add_path: "string -> Name_Space.naming -> Name_Space.naming"} \\
   @{index_ML Name_Space.full_name: "Name_Space.naming -> binding -> string"} \\
   \end{mldecls}
@@ -975,9 +975,9 @@
   \item Type @{ML_type Name_Space.naming} represents the abstract
   concept of a naming policy.
 
-  \item @{ML Name_Space.default_naming} is the default naming policy.
-  In a theory context, this is usually augmented by a path prefix
-  consisting of the theory name.
+  \item @{ML Name_Space.global_naming} is the default naming policy: it is
+  global and lacks any path prefix.  In a regular theory context this is
+  augmented by a path prefix consisting of the theory name.
 
   \item @{ML Name_Space.add_path}~@{text "path naming"} augments the
   naming policy by extending its path component.

--- a/src/Pure/General/name_space.ML	Mon Oct 13 21:57:40 2014 +0200
+++ b/src/Pure/General/name_space.ML	Mon Oct 13 22:43:29 2014 +0200
@@ -44,7 +44,7 @@
   val parent_path: naming -> naming
   val mandatory_path: string -> naming -> naming
   val qualified_path: bool -> binding -> naming -> naming
-  val default_naming: naming
+  val global_naming: naming
   val local_naming: naming
   val transform_binding: naming -> binding -> binding
   val full_name: naming -> binding -> string
@@ -324,8 +324,8 @@
 fun qualified_path mandatory binding = map_path (fn path =>
   path @ #2 (Binding.dest (Binding.qualified mandatory "" binding)));
 
-val default_naming = make_naming (false, NONE, "", []);
-val local_naming = default_naming |> add_path Long_Name.localN;
+val global_naming = make_naming (false, NONE, "", []);
+val local_naming = global_naming |> add_path Long_Name.localN;
 
 
 (* full name *)
@@ -354,7 +354,7 @@
 fun full_name naming =
   name_spec naming #> #2 #> map #1 #> Long_Name.implode;
 
-val base_name = full_name default_naming #> Long_Name.base_name;
+val base_name = full_name global_naming #> Long_Name.base_name;
 
 
 (* accesses *)
@@ -411,9 +411,9 @@
 structure Data_Args =
 struct
   type T = naming;
-  val empty = default_naming;
-  fun extend _ = default_naming;
-  fun merge _ = default_naming;
+  val empty = global_naming;
+  fun extend _ = global_naming;
+  fun merge _ = global_naming;
   fun init _ = local_naming;
 end;
 

--- a/src/Pure/Isar/class.ML	Mon Oct 13 21:57:40 2014 +0200
+++ b/src/Pure/Isar/class.ML	Mon Oct 13 22:43:29 2014 +0200
@@ -326,7 +326,7 @@
 fun guess_morphism_identity (b, rhs) phi1 phi2 =
   let
     (*FIXME proper concept to identify morphism instead of educated guess*)
-    val name_of_binding = Name_Space.full_name Name_Space.default_naming;
+    val name_of_binding = Name_Space.full_name Name_Space.global_naming;
     val n1 = (name_of_binding o Morphism.binding phi1) b;
     val n2 = (name_of_binding o Morphism.binding phi2) b;
     val rhs1 = Morphism.term phi1 rhs;

--- a/src/Pure/Isar/proof_context.ML	Mon Oct 13 21:57:40 2014 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Oct 13 22:43:29 2014 +0200
@@ -1197,7 +1197,7 @@
 
 fun update_cases is_proper args ctxt =
   let
-    val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.default_naming);
+    val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming);
     val cases = cases_of ctxt;
     val index = Name_Space.fold_table (fn _ => Integer.add 1) cases 0;
     val (cases', _) = fold (update_case context is_proper) args (cases, index);

--- a/src/Pure/Tools/plugin.ML	Mon Oct 13 21:57:40 2014 +0200
+++ b/src/Pure/Tools/plugin.ML	Mon Oct 13 22:43:29 2014 +0200
@@ -54,7 +54,7 @@
 
 fun define binding rhs thy =
   let
-    val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.default_naming);
+    val context = Context.Theory thy |> Name_Space.map_naming (K Name_Space.global_naming);
     val (name, data') = Name_Space.define context true (binding, resolve thy rhs) (Data.get thy);
     val thy' = Data.put data' thy;
   in (name, thy') end;

--- a/src/Pure/variable.ML	Mon Oct 13 21:57:40 2014 +0200
+++ b/src/Pure/variable.ML	Mon Oct 13 22:43:29 2014 +0200
@@ -380,11 +380,11 @@
 fun new_fixed ((x, x'), pos) ctxt =
   if is_some (lookup_fixed ctxt x') then err_dups [Binding.make (x, pos)]
   else
-    let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.default_naming) in
+    let val context = Context.Proof ctxt |> Name_Space.map_naming (K Name_Space.global_naming) in
       ctxt
       |> map_fixes
         (Name_Space.define context true (Binding.make (x', pos), x) #> snd #>
-          Name_Space.alias_table Name_Space.default_naming (Binding.make (x, pos)) x')
+          Name_Space.alias_table Name_Space.global_naming (Binding.make (x, pos)) x')
       |> declare_fixed x
       |> declare_constraints (Syntax.free x')
   end;