Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;

--- a/NEWS	Sat Apr 16 12:46:18 2011 +0200
+++ b/NEWS	Sat Apr 16 13:48:45 2011 +0200
@@ -37,6 +37,13 @@
 Note that automated detection from the file-system or search path has
 been discontinued.  INCOMPATIBILITY.
 
+* Name space: proper configuration options "long_names",
+"short_names", "unique_names" instead of former unsynchronized
+references.  Minor INCOMPATIBILITY, need to declare options in context
+like this:
+
+  declare [[unique_names = false]]
+
 
 *** HOL ***
 

--- a/doc-src/Codegen/Thy/Setup.thy	Sat Apr 16 12:46:18 2011 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy	Sat Apr 16 13:48:45 2011 +0200
@@ -22,6 +22,6 @@
 
 setup {* Code_Target.set_default_code_width 74 *}
 
-ML_command {* unique_names := false *}
+declare [[unique_names = false]]
 
 end

--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Apr 16 12:46:18 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Apr 16 13:48:45 2011 +0200
@@ -1112,7 +1112,7 @@
   @{index_ML Name_Space.declare: "bool -> Name_Space.naming -> binding -> Name_Space.T ->
   string * Name_Space.T"} \\
   @{index_ML Name_Space.intern: "Name_Space.T -> string -> string"} \\
-  @{index_ML Name_Space.extern: "Name_Space.T -> string -> string"} \\
+  @{index_ML Name_Space.extern: "Proof.context -> Name_Space.T -> string -> string"} \\
   @{index_ML Name_Space.is_concealed: "Name_Space.T -> string -> bool"}
   \end{mldecls}
 
@@ -1187,7 +1187,7 @@
   (or their derivatives for @{ML_type theory} and
   @{ML_type Proof.context}).
 
-  \item @{ML Name_Space.extern}~@{text "space name"} externalizes a
+  \item @{ML Name_Space.extern}~@{text "ctxt space name"} externalizes a
   (fully qualified) internal name.
 
   This operation is mostly for printing!  User code should not rely on

--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sat Apr 16 12:46:18 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sat Apr 16 13:48:45 2011 +0200
@@ -1610,7 +1610,7 @@
   \indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: bool -> Name_Space.naming -> binding -> Name_Space.T ->|\isasep\isanewline%
 \verb|  string * Name_Space.T| \\
   \indexdef{}{ML}{Name\_Space.intern}\verb|Name_Space.intern: Name_Space.T -> string -> string| \\
-  \indexdef{}{ML}{Name\_Space.extern}\verb|Name_Space.extern: Name_Space.T -> string -> string| \\
+  \indexdef{}{ML}{Name\_Space.extern}\verb|Name_Space.extern: Proof.context -> Name_Space.T -> string -> string| \\
   \indexdef{}{ML}{Name\_Space.is\_concealed}\verb|Name_Space.is_concealed: Name_Space.T -> string -> bool|
   \end{mldecls}
 
@@ -1679,7 +1679,7 @@
   (or their derivatives for \verb|theory| and
   \verb|Proof.context|).
 
-  \item \verb|Name_Space.extern|~\isa{space\ name} externalizes a
+  \item \verb|Name_Space.extern|~\isa{ctxt\ space\ name} externalizes a
   (fully qualified) internal name.
 
   This operation is mostly for printing!  User code should not rely on

--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat Apr 16 12:46:18 2011 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat Apr 16 13:48:45 2011 +0200
@@ -100,10 +100,10 @@
     @{index_ML show_sorts: "bool Config.T"} & default @{ML false} \\
     @{index_ML show_consts: "bool Config.T"} & default @{ML false} \\
     @{index_ML show_abbrevs: "bool Config.T"} & default @{ML true} \\
-    @{index_ML long_names: "bool Unsynchronized.ref"} & default @{ML false} \\
-    @{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\
-    @{index_ML unique_names: "bool Unsynchronized.ref"} & default @{ML true} \\
     @{index_ML show_brackets: "bool Config.T"} & default @{ML false} \\
+    @{index_ML Name_Space.long_names: "bool Config.T"} & default @{ML false} \\
+    @{index_ML Name_Space.short_names: "bool Config.T"} & default @{ML false} \\
+    @{index_ML Name_Space.unique_names: "bool Config.T"} & default @{ML true} \\
     @{index_ML eta_contract: "bool Config.T"} & default @{ML true} \\
     @{index_ML Goal_Display.goals_limit: "int Config.T"} & default @{ML 10} \\
     @{index_ML Goal_Display.show_main_goal: "bool Config.T"} & default @{ML false} \\
@@ -144,11 +144,6 @@
 
   \item @{ML show_abbrevs} controls folding of constant abbreviations.
 
-  \item @{ML long_names}, @{ML short_names}, and @{ML unique_names}
-  control the way of printing fully qualified internal names in
-  external form.  See also \secref{sec:antiq} for the document
-  antiquotation options of the same names.
-
   \item @{ML show_brackets} controls bracketing in pretty printed
   output.  If set to @{ML true}, all sub-expressions of the pretty
   printing tree will be parenthesized, even if this produces malformed
@@ -156,6 +151,12 @@
   pretty printed entities may occasionally help to diagnose problems
   with operator priorities, for example.
 
+  \item @{ML Name_Space.long_names}, @{ML Name_Space.short_names}, and
+  @{ML Name_Space.unique_names} control the way of printing fully
+  qualified internal names in external form.  See also
+  \secref{sec:antiq} for the document antiquotation options of the
+  same names.
+
   \item @{ML eta_contract} controls @{text "\<eta>"}-contracted printing of
   terms.
 

--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat Apr 16 12:46:18 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat Apr 16 13:48:45 2011 +0200
@@ -122,10 +122,10 @@
     \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Config.T| & default \verb|false| \\
     \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & default \verb|false| \\
     \indexdef{}{ML}{show\_abbrevs}\verb|show_abbrevs: bool Config.T| & default \verb|true| \\
-    \indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\
-    \indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\
-    \indexdef{}{ML}{unique\_names}\verb|unique_names: bool Unsynchronized.ref| & default \verb|true| \\
     \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool Config.T| & default \verb|false| \\
+    \indexdef{}{ML}{Name\_Space.long\_names}\verb|Name_Space.long_names: bool Config.T| & default \verb|false| \\
+    \indexdef{}{ML}{Name\_Space.short\_names}\verb|Name_Space.short_names: bool Config.T| & default \verb|false| \\
+    \indexdef{}{ML}{Name\_Space.unique\_names}\verb|Name_Space.unique_names: bool Config.T| & default \verb|true| \\
     \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool Config.T| & default \verb|true| \\
     \indexdef{}{ML}{Goal\_Display.goals\_limit}\verb|Goal_Display.goals_limit: int Config.T| & default \verb|10| \\
     \indexdef{}{ML}{Goal\_Display.show\_main\_goal}\verb|Goal_Display.show_main_goal: bool Config.T| & default \verb|false| \\
@@ -165,11 +165,6 @@
 
   \item \verb|show_abbrevs| controls folding of constant abbreviations.
 
-  \item \verb|long_names|, \verb|short_names|, and \verb|unique_names|
-  control the way of printing fully qualified internal names in
-  external form.  See also \secref{sec:antiq} for the document
-  antiquotation options of the same names.
-
   \item \verb|show_brackets| controls bracketing in pretty printed
   output.  If set to \verb|true|, all sub-expressions of the pretty
   printing tree will be parenthesized, even if this produces malformed
@@ -177,6 +172,12 @@
   pretty printed entities may occasionally help to diagnose problems
   with operator priorities, for example.
 
+  \item \verb|Name_Space.long_names|, \verb|Name_Space.short_names|, and
+  \verb|Name_Space.unique_names| control the way of printing fully
+  qualified internal names in external form.  See also
+  \secref{sec:antiq} for the document antiquotation options of the
+  same names.
+
   \item \verb|eta_contract| controls \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-contracted printing of
   terms.
 

--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Sat Apr 16 12:46:18 2011 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Sat Apr 16 13:48:45 2011 +0200
@@ -152,11 +152,8 @@
 the qualified name, for example @{text "T.length"}, where @{text T} is the
 theory it is defined in, to distinguish it from the predefined @{const[source]
 "List.length"}. In case there is no danger of confusion, you can insist on
-short names (no qualifiers) by setting \verb!short_names!, typically
-in \texttt{ROOT.ML}:
-\begin{quote}
-@{ML "short_names := true"}\verb!;!
-\end{quote}
+short names (no qualifiers) by setting the \verb!short_names!
+configuration option in the context.
 *}
 
 subsection {*Variable names\label{sec:varnames}*}

--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Sat Apr 16 12:46:18 2011 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Sat Apr 16 13:48:45 2011 +0200
@@ -195,11 +195,8 @@
 If there are multiple declarations of the same name, Isabelle prints
 the qualified name, for example \isa{T{\isaliteral{2E}{\isachardot}}length}, where \isa{T} is the
 theory it is defined in, to distinguish it from the predefined \isa{{\isaliteral{22}{\isachardoublequote}}List{\isaliteral{2E}{\isachardot}}length{\isaliteral{22}{\isachardoublequote}}}. In case there is no danger of confusion, you can insist on
-short names (no qualifiers) by setting \verb!short_names!, typically
-in \texttt{ROOT.ML}:
-\begin{quote}
-\verb|short_names := true|\verb!;!
-\end{quote}%
+short names (no qualifiers) by setting the \verb!short_names!
+configuration option in the context.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

--- a/doc-src/TutorialI/Misc/Itrev.thy	Sat Apr 16 12:46:18 2011 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Sat Apr 16 13:48:45 2011 +0200
@@ -2,7 +2,7 @@
 theory Itrev
 imports Main
 begin
-ML"unique_names := false"
+declare [[unique_names = false]]
 (*>*)
 
 section{*Induction Heuristics*}
@@ -141,6 +141,6 @@
 \index{induction heuristics|)}
 *}
 (*<*)
-ML"unique_names := true"
+declare [[unique_names = true]]
 end
 (*>*)

--- a/doc-src/TutorialI/Misc/document/Itrev.tex	Sat Apr 16 12:46:18 2011 +0200
+++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Sat Apr 16 13:48:45 2011 +0200
@@ -15,19 +15,6 @@
 %
 \endisadelimtheory
 %
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
 \isamarkupsection{Induction Heuristics%
 }
 \isamarkuptrue%
@@ -216,19 +203,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isadelimML
-%
-\endisadelimML
-%
-\isatagML
-%
-\endisatagML
-{\isafoldML}%
-%
-\isadelimML
-%
-\endisadelimML
-%
 \isadelimtheory
 %
 \endisadelimtheory

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -848,8 +848,8 @@
                             th |> backquote_thm
                           else
                             let
-                              val name1 = Facts.extern facts name0
-                              val name2 = Name_Space.extern full_space name0
+                              val name1 = Facts.extern ctxt facts name0
+                              val name2 = Name_Space.extern ctxt full_space name0
                             in
                               case find_first check_thms [name1, name2, name0] of
                                 SOME name => make_name reserved multi j name

--- a/src/HOL/Tools/inductive.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/HOL/Tools/inductive.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -151,7 +151,7 @@
     val (tab, monos) = get_inductives ctxt;
     val space = Consts.space_of (ProofContext.consts_of ctxt);
   in
-    [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table (space, tab))),
+    [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table ctxt (space, tab))),
      Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
     |> Pretty.chunks |> Pretty.writeln
   end;

--- a/src/HOL/Tools/record.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/HOL/Tools/record.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -914,7 +914,7 @@
 fun record_tr' ctxt t =
   let
     val thy = ProofContext.theory_of ctxt;
-    val extern = Consts.extern (ProofContext.consts_of ctxt);
+    val extern = Consts.extern ctxt (ProofContext.consts_of ctxt);
 
     fun strip_fields t =
       (case strip_comb t of
@@ -957,7 +957,7 @@
 
 fun dest_update ctxt c =
   (case try Lexicon.unmark_const c of
-    SOME d => try (unsuffix updateN) (Consts.extern (ProofContext.consts_of ctxt) d)
+    SOME d => try (unsuffix updateN) (Consts.extern ctxt (ProofContext.consts_of ctxt) d)
   | NONE => NONE);
 
 fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =

--- a/src/Pure/General/name_space.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/General/name_space.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -7,16 +7,8 @@
 
 type xstring = string;    (*external names*)
 
-signature BASIC_NAME_SPACE =
-sig
-  val long_names: bool Unsynchronized.ref
-  val short_names: bool Unsynchronized.ref
-  val unique_names: bool Unsynchronized.ref
-end;
-
 signature NAME_SPACE =
 sig
-  include BASIC_NAME_SPACE
   val hidden: string -> string
   val is_hidden: string -> bool
   type T
@@ -27,9 +19,16 @@
   val markup_entry: T -> string -> Markup.T
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
-  val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
-    T -> string -> xstring
-  val extern: T -> string -> xstring
+  val long_names_default: bool Unsynchronized.ref
+  val long_names_raw: Config.raw
+  val long_names: bool Config.T
+  val short_names_default: bool Unsynchronized.ref
+  val short_names_raw: Config.raw
+  val short_names: bool Config.T
+  val unique_names_default: bool Unsynchronized.ref
+  val unique_names_raw: Config.raw
+  val unique_names: bool Config.T
+  val extern: Proof.context -> T -> string -> xstring
   val hide: bool -> string -> T -> T
   val merge: T * T -> T
   type naming
@@ -55,8 +54,8 @@
   val merge_tables: 'a table * 'a table -> 'a table
   val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
     'a table * 'a table -> 'a table
-  val dest_table: 'a table -> (string * 'a) list
-  val extern_table: 'a table -> (xstring * 'a) list
+  val dest_table: Proof.context -> 'a table -> (string * 'a) list
+  val extern_table: Proof.context -> 'a table -> (xstring * 'a) list
 end;
 
 structure Name_Space: NAME_SPACE =
@@ -154,8 +153,25 @@
 
 fun intern space xname = #1 (lookup space xname);
 
-fun extern_flags {long_names, short_names, unique_names} space name =
+
+val long_names_default = Unsynchronized.ref false;
+val long_names_raw = Config.declare "long_names" (fn _ => Config.Bool (! long_names_default));
+val long_names = Config.bool long_names_raw;
+
+val short_names_default = Unsynchronized.ref false;
+val short_names_raw = Config.declare "short_names" (fn _ => Config.Bool (! short_names_default));
+val short_names = Config.bool short_names_raw;
+
+val unique_names_default = Unsynchronized.ref true;
+val unique_names_raw = Config.declare "unique_names" (fn _ => Config.Bool (! unique_names_default));
+val unique_names = Config.bool unique_names_raw;
+
+fun extern ctxt space name =
   let
+    val long_names = Config.get ctxt long_names;
+    val short_names = Config.get ctxt short_names;
+    val unique_names = Config.get ctxt unique_names;
+
     fun valid require_unique xname =
       let val (name', is_unique) = lookup space xname
       in name = name' andalso (not require_unique orelse is_unique) end;
@@ -168,16 +184,6 @@
     else ext (get_accesses space name)
   end;
 
-val long_names = Unsynchronized.ref false;
-val short_names = Unsynchronized.ref false;
-val unique_names = Unsynchronized.ref true;
-
-fun extern space name =
-  extern_flags
-   {long_names = ! long_names,
-    short_names = ! short_names,
-    unique_names = ! unique_names} space name;
-
 
 (* modify internals *)
 
@@ -385,15 +391,12 @@
 fun join_tables f ((space1, tab1), (space2, tab2)) =
   (merge (space1, space2), Symtab.join f (tab1, tab2));
 
-fun ext_table (space, tab) =
-  Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
+fun ext_table ctxt (space, tab) =
+  Symtab.fold (fn (name, x) => cons ((name, extern ctxt space name), x)) tab []
   |> Library.sort_wrt (#2 o #1);
 
-fun dest_table tab = map (apfst #1) (ext_table tab);
-fun extern_table tab = map (apfst #2) (ext_table tab);
+fun dest_table ctxt tab = map (apfst #1) (ext_table ctxt tab);
+fun extern_table ctxt tab = map (apfst #2) (ext_table ctxt tab);
 
 end;
 
-structure Basic_Name_Space: BASIC_NAME_SPACE = Name_Space;
-open Basic_Name_Space;
-

--- a/src/Pure/Isar/attrib.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -73,11 +73,12 @@
 
 fun print_attributes thy =
   let
+    val ctxt = ProofContext.init_global thy;
     val attribs = Attributes.get thy;
     fun prt_attr (name, (_, comment)) = Pretty.block
       [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   in
-    [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table attribs))]
+    [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table ctxt attribs))]
     |> Pretty.chunks |> Pretty.writeln
   end;
 
@@ -90,7 +91,7 @@
 val intern = Name_Space.intern o #1 o Attributes.get;
 val intern_src = Args.map_name o intern;
 
-val extern = Name_Space.extern o #1 o Attributes.get o ProofContext.theory_of;
+fun extern ctxt = Name_Space.extern ctxt (#1 (Attributes.get (ProofContext.theory_of ctxt)));
 
 
 (* pretty printing *)
@@ -341,7 +342,7 @@
         Pretty.block [Pretty.str (name ^ ": " ^ Config.print_type value ^ " ="), Pretty.brk 1,
           Pretty.str (Config.print_value value)]
       end;
-    val configs = Name_Space.extern_table (#1 (Attributes.get thy), Configs.get thy);
+    val configs = Name_Space.extern_table ctxt (#1 (Attributes.get thy), Configs.get thy);
   in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
 
 
@@ -408,6 +409,9 @@
   register_config Printer.show_question_marks_raw #>
   register_config Syntax.ambiguity_level_raw #>
   register_config Syntax_Trans.eta_contract_raw #>
+  register_config Name_Space.long_names_raw #>
+  register_config Name_Space.short_names_raw #>
+  register_config Name_Space.unique_names_raw #>
   register_config ML_Context.trace_raw #>
   register_config ProofContext.show_abbrevs_raw #>
   register_config Goal_Display.goals_limit_raw #>

--- a/src/Pure/Isar/expression.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/Isar/expression.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -616,7 +616,7 @@
 fun aprop_tr' n c = (Lexicon.mark_const c, fn ctxt => fn args =>
   if length args = n then
     Syntax.const "_aprop" $   (* FIXME avoid old-style early externing (!??) *)
-      Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
+      Term.list_comb (Syntax.free (Consts.extern ctxt (ProofContext.consts_of ctxt) c), args)
   else raise Match);
 
 (* define one predicate including its intro rule and axioms

--- a/src/Pure/Isar/isar_cmd.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -399,11 +399,11 @@
 
 val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   let
-    val thy = Toplevel.theory_of state;
-    val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy);
+    val ctxt = Toplevel.context_of state;
+    val {classes = (space, algebra), ...} = Type.rep_tsig (ProofContext.tsig_of ctxt);
     val classes = Sorts.classes_of algebra;
     fun entry (c, (i, (_, cs))) =
-      (i, {name = Name_Space.extern space c, ID = c, parents = cs,
+      (i, {name = Name_Space.extern ctxt space c, ID = c, parents = cs,
             dir = "", unfold = true, path = ""});
     val gr =
       Graph.fold (cons o entry) classes []

--- a/src/Pure/Isar/locale.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/Isar/locale.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -162,7 +162,7 @@
 );
 
 val intern = Name_Space.intern o #1 o Locales.get;
-val extern = Name_Space.extern o #1 o Locales.get;
+fun extern thy = Name_Space.extern (ProofContext.init_global thy) (#1 (Locales.get thy));
 
 val get_locale = Symtab.lookup o #2 o Locales.get;
 val defined = Symtab.defined o #2 o Locales.get;
@@ -630,7 +630,8 @@
 val all_locales = Symtab.keys o snd o Locales.get;
 
 fun print_locales thy =
-  Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy)))
+  Pretty.strs ("locales:" ::
+    map #1 (Name_Space.extern_table (ProofContext.init_global thy) (Locales.get thy)))
   |> Pretty.writeln;
 
 fun print_locale thy show_facts raw_name =

--- a/src/Pure/Isar/method.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/Isar/method.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -334,11 +334,12 @@
 
 fun print_methods thy =
   let
+    val ctxt = ProofContext.init_global thy;
     val meths = Methods.get thy;
     fun prt_meth (name, (_, comment)) = Pretty.block
       [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   in
-    [Pretty.big_list "methods:" (map prt_meth (Name_Space.extern_table meths))]
+    [Pretty.big_list "methods:" (map prt_meth (Name_Space.extern_table ctxt meths))]
     |> Pretty.chunks |> Pretty.writeln
   end;
 

--- a/src/Pure/Isar/proof_context.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -304,8 +304,8 @@
     val global_facts = Global_Theory.facts_of (theory_of ctxt);
   in
     if is_some (Facts.lookup (Context.Proof ctxt) local_facts name)
-    then Facts.extern local_facts name
-    else Facts.extern global_facts name
+    then Facts.extern ctxt local_facts name
+    else Facts.extern ctxt global_facts name
   end;
 
 
@@ -1152,7 +1152,8 @@
       | add_abbr (c, (T, SOME t)) =
           if not show_globals andalso Symtab.defined globals c then I
           else cons (c, Logic.mk_equals (Const (c, T), t));
-    val abbrevs = Name_Space.extern_table (space, Symtab.make (Symtab.fold add_abbr consts []));
+    val abbrevs =
+      Name_Space.extern_table ctxt (space, Symtab.make (Symtab.fold add_abbr consts []));
   in
     if null abbrevs then []
     else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]

--- a/src/Pure/ProofGeneral/preferences.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -124,7 +124,7 @@
   bool_pref Goal_Display.show_consts_default
     "show-consts"
     "Show types of consts in Isabelle goal display",
-  bool_pref long_names
+  bool_pref Name_Space.long_names_default
     "long-names"
     "Show fully qualified names in Isabelle terms",
   bool_pref Printer.show_brackets_default

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -517,12 +517,15 @@
 
 local
 
-fun theory_facts name =
+fun theory_facts thy =
+  (map Global_Theory.facts_of (Theory.parents_of thy), Global_Theory.facts_of thy);
+
+fun thms_of_thy name =
   let val thy = Thy_Info.get_theory name
-  in (map Global_Theory.facts_of (Theory.parents_of thy), Global_Theory.facts_of thy) end;
+  in map fst (theory_facts thy |-> Facts.extern_static (ProofContext.init_global thy)) end;
 
-fun thms_of_thy name = map fst (theory_facts name |-> Facts.extern_static);
-fun qualified_thms_of_thy name = map fst (theory_facts name |-> Facts.dest_static);
+fun qualified_thms_of_thy name =
+  map fst (theory_facts (Thy_Info.get_theory name) |-> Facts.dest_static);
 
 in
 

--- a/src/Pure/Syntax/syntax_phases.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -605,6 +605,8 @@
 fun unparse_t t_to_ast prt_t markup ctxt t =
   let
     val syn = ProofContext.syn_of ctxt;
+    val tsig = ProofContext.tsig_of ctxt;
+    val consts = ProofContext.consts_of ctxt;
 
     fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
       | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
@@ -620,9 +622,9 @@
         SOME "" => ([], c)
       | SOME b => markup_extern b
       | NONE => c |> Lexicon.unmark
-         {case_class = fn x => ([Markup.tclass x], Type.extern_class (ProofContext.tsig_of ctxt) x),
-          case_type = fn x => ([Markup.tycon x], Type.extern_type (ProofContext.tsig_of ctxt) x),
-          case_const = fn x => ([Markup.const x], Consts.extern (ProofContext.consts_of ctxt) x),
+         {case_class = fn x => ([Markup.tclass x], Type.extern_class ctxt tsig x),
+          case_type = fn x => ([Markup.tycon x], Type.extern_type ctxt tsig x),
+          case_const = fn x => ([Markup.const x], Consts.extern ctxt consts x),
           case_fixed = fn x => free_or_skolem ctxt x,
           case_default = fn x => ([], x)});
   in

--- a/src/Pure/Thy/thy_output.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -450,9 +450,9 @@
 val _ = add_option "show_structs" (Config.put show_structs o boolean);
 val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
 val _ = add_option "show_abbrevs" (Config.put show_abbrevs o boolean);
-val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
-val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);
-val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);
+val _ = add_option "long_names" (Config.put Name_Space.long_names o boolean);
+val _ = add_option "short_names" (Config.put Name_Space.short_names o boolean);
+val _ = add_option "unique_names" (Config.put Name_Space.unique_names o boolean);
 val _ = add_option "eta_contract" (Config.put Syntax_Trans.eta_contract o boolean);
 val _ = add_option "display" (Config.put display o boolean);
 val _ = add_option "break" (Config.put break o boolean);
@@ -510,11 +510,11 @@
   in ProofContext.pretty_term_abbrev ctxt' eq end;
 
 fun pretty_class ctxt =
-  Pretty.str o Type.extern_class (ProofContext.tsig_of ctxt) o ProofContext.read_class ctxt;
+  Pretty.str o Type.extern_class ctxt (ProofContext.tsig_of ctxt) o ProofContext.read_class ctxt;
 
 fun pretty_type ctxt s =
   let val Type (name, _) = ProofContext.read_type_name_proper ctxt false s
-  in Pretty.str (Type.extern_type (ProofContext.tsig_of ctxt) name) end;
+  in Pretty.str (Type.extern_type ctxt (ProofContext.tsig_of ctxt) name) end;
 
 fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
 

--- a/src/Pure/Tools/find_theorems.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -381,8 +381,11 @@
     val space = Facts.space_of (Global_Theory.facts_of (ProofContext.theory_of ctxt));
 
     val shorten =
-      Name_Space.extern_flags
-        {long_names = false, short_names = false, unique_names = false} space;
+      Name_Space.extern
+        (ctxt
+          |> Config.put Name_Space.long_names false
+          |> Config.put Name_Space.short_names false
+          |> Config.put Name_Space.unique_names false) space;
 
     fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
           nicer_name (shorten x, i) (shorten y, j)

--- a/src/Pure/consts.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/consts.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -22,9 +22,9 @@
   val alias: Name_Space.naming -> binding -> string -> T -> T
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
-  val extern: T -> string -> xstring
+  val extern: Proof.context -> T -> string -> xstring
   val intern_syntax: T -> xstring -> string
-  val extern_syntax: T -> string -> xstring
+  val extern_syntax: Proof.context -> T -> string -> xstring
   val read_const: T -> string -> term
   val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   val typargs: T -> string * typ -> typ list
@@ -129,16 +129,16 @@
 val is_concealed = Name_Space.is_concealed o space_of;
 
 val intern = Name_Space.intern o space_of;
-val extern = Name_Space.extern o space_of;
+fun extern ctxt = Name_Space.extern ctxt o space_of;
 
 fun intern_syntax consts s =
   (case try Lexicon.unmark_const s of
     SOME c => c
   | NONE => intern consts s);
 
-fun extern_syntax consts s =
+fun extern_syntax ctxt consts s =
   (case try Lexicon.unmark_const s of
-    SOME c => extern consts c
+    SOME c => extern ctxt consts c
   | NONE => s);
 
 

--- a/src/Pure/display.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/display.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -187,25 +187,25 @@
     val {restricts, reducts} = Defs.dest defs;
     val {naming = _, syn = _, tsig, consts} = Sign.rep_sg thy;
     val {constants, constraints} = Consts.dest consts;
-    val extern_const = Name_Space.extern (#1 constants);
+    val extern_const = Name_Space.extern ctxt (#1 constants);
     val {classes, default, types, ...} = Type.rep_tsig tsig;
     val (class_space, class_algebra) = classes;
     val classes = Sorts.classes_of class_algebra;
     val arities = Sorts.arities_of class_algebra;
 
-    val clsses = Name_Space.dest_table (class_space, Symtab.make (Graph.dest classes));
-    val tdecls = Name_Space.dest_table types;
-    val arties = Name_Space.dest_table (Sign.type_space thy, arities);
+    val clsses = Name_Space.dest_table ctxt (class_space, Symtab.make (Graph.dest classes));
+    val tdecls = Name_Space.dest_table ctxt types;
+    val arties = Name_Space.dest_table ctxt (Sign.type_space thy, arities);
 
     fun prune_const c = not verbose andalso Consts.is_concealed consts c;
-    val cnsts = Name_Space.extern_table (#1 constants,
+    val cnsts = Name_Space.extern_table ctxt (#1 constants,
       Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants))));
 
     val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
     val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
-    val cnstrs = Name_Space.extern_table constraints;
+    val cnstrs = Name_Space.extern_table ctxt constraints;
 
-    val axms = Name_Space.extern_table axioms;
+    val axms = Name_Space.extern_table ctxt axioms;
 
     val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
       |> map (fn (lhs, rhs) =>
@@ -225,7 +225,7 @@
       Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
       Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
       Pretty.big_list "axioms:" (map pretty_axm axms),
-      Pretty.strs ("oracles:" :: Thm.extern_oracles thy),
+      Pretty.strs ("oracles:" :: Thm.extern_oracles ctxt),
       Pretty.big_list "definitions:"
         [pretty_finals reds0,
          Pretty.big_list "non-overloaded:" (map pretty_reduct reds1),

--- a/src/Pure/facts.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/facts.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -23,12 +23,12 @@
   val space_of: T -> Name_Space.T
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
-  val extern: T -> string -> xstring
+  val extern: Proof.context -> T -> string -> xstring
   val lookup: Context.generic -> T -> string -> (bool * thm list) option
   val defined: T -> string -> bool
   val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
   val dest_static: T list -> T -> (string * thm list) list
-  val extern_static: T list -> T -> (xstring * thm list) list
+  val extern_static: Proof.context -> T list -> T -> (xstring * thm list) list
   val props: T -> thm list
   val could_unify: T -> term -> thm list
   val merge: T * T -> T
@@ -141,7 +141,7 @@
 val is_concealed = Name_Space.is_concealed o space_of;
 
 val intern = Name_Space.intern o space_of;
-val extern = Name_Space.extern o space_of;
+fun extern ctxt = Name_Space.extern ctxt o space_of;
 
 val defined = Symtab.defined o table_of;
 
@@ -165,8 +165,8 @@
 fun dest_static prev_facts facts =
   sort_wrt #1 (diff_table prev_facts facts);
 
-fun extern_static prev_facts facts =
-  sort_wrt #1 (diff_table prev_facts facts |> map (apfst (extern facts)));
+fun extern_static ctxt prev_facts facts =
+  sort_wrt #1 (diff_table prev_facts facts |> map (apfst (extern ctxt facts)));
 
 
 (* indexed props *)

--- a/src/Pure/sign.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/sign.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -233,11 +233,11 @@
 fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy;
 
 val intern_class = Name_Space.intern o class_space;
-val extern_class = Name_Space.extern o class_space;
+fun extern_class thy = Name_Space.extern (ProofContext.init_global thy) (class_space thy);
 val intern_type = Name_Space.intern o type_space;
-val extern_type = Name_Space.extern o type_space;
+fun extern_type thy = Name_Space.extern (ProofContext.init_global thy) (type_space thy);
 val intern_const = Name_Space.intern o const_space;
-val extern_const = Name_Space.extern o const_space;
+fun extern_const thy = Name_Space.extern (ProofContext.init_global thy) (const_space thy);
 
 
 

--- a/src/Pure/thm.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/thm.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -147,7 +147,7 @@
   val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
   val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
   val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
-  val extern_oracles: theory -> xstring list
+  val extern_oracles: Proof.context -> xstring list
   val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
 end;
 
@@ -1734,7 +1734,8 @@
   fun merge data : T = Name_Space.merge_tables data;
 );
 
-val extern_oracles = map #1 o Name_Space.extern_table o Oracles.get;
+fun extern_oracles ctxt =
+  map #1 (Name_Space.extern_table ctxt (Oracles.get (ProofContext.theory_of ctxt)));
 
 fun add_oracle (b, oracle) thy =
   let

--- a/src/Pure/type.ML	Sat Apr 16 12:46:18 2011 +0200
+++ b/src/Pure/type.ML	Sat Apr 16 13:48:45 2011 +0200
@@ -28,7 +28,7 @@
   val class_space: tsig -> Name_Space.T
   val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
   val intern_class: tsig -> xstring -> string
-  val extern_class: tsig -> string -> xstring
+  val extern_class: Proof.context -> tsig -> string -> xstring
   val defaultS: tsig -> sort
   val logical_types: tsig -> string list
   val eq_sort: tsig -> sort * sort -> bool
@@ -49,7 +49,7 @@
   val type_space: tsig -> Name_Space.T
   val type_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
   val intern_type: tsig -> xstring -> string
-  val extern_type: tsig -> string -> xstring
+  val extern_type: Proof.context -> tsig -> string -> xstring
   val is_logtype: tsig -> string -> bool
   val the_decl: tsig -> string -> decl
   val cert_typ_mode: mode -> tsig -> typ -> typ
@@ -192,7 +192,7 @@
   ((Name_Space.alias naming binding name space, classes), default, types));
 
 val intern_class = Name_Space.intern o class_space;
-val extern_class = Name_Space.extern o class_space;
+fun extern_class ctxt = Name_Space.extern ctxt o class_space;
 
 fun defaultS (TSig {default, ...}) = default;
 fun logical_types (TSig {log_types, ...}) = log_types;
@@ -237,7 +237,7 @@
   (classes, default, (Name_Space.alias naming binding name space, types)));
 
 val intern_type = Name_Space.intern o type_space;
-val extern_type = Name_Space.extern o type_space;
+fun extern_type ctxt = Name_Space.extern ctxt o type_space;
 
 val is_logtype = member (op =) o logical_types;