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