Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
authorwenzelm
Sat Apr 16 13:48:45 2011 +0200 (2011-04-16)
changeset 42358b47d41d9f4b5
parent 42357 3305f573294e
child 42359 6ca5407863ed
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
NEWS
doc-src/Codegen/Thy/Setup.thy
doc-src/IsarImplementation/Thy/Prelim.thy
doc-src/IsarImplementation/Thy/document/Prelim.tex
doc-src/IsarRef/Thy/Inner_Syntax.thy
doc-src/IsarRef/Thy/document/Inner_Syntax.tex
doc-src/LaTeXsugar/Sugar/Sugar.thy
doc-src/LaTeXsugar/Sugar/document/Sugar.tex
doc-src/TutorialI/Misc/Itrev.thy
doc-src/TutorialI/Misc/document/Itrev.tex
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/record.ML
src/Pure/General/name_space.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof_context.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Thy/thy_output.ML
src/Pure/Tools/find_theorems.ML
src/Pure/consts.ML
src/Pure/display.ML
src/Pure/facts.ML
src/Pure/sign.ML
src/Pure/thm.ML
src/Pure/type.ML
     1.1 --- a/NEWS	Sat Apr 16 12:46:18 2011 +0200
     1.2 +++ b/NEWS	Sat Apr 16 13:48:45 2011 +0200
     1.3 @@ -37,6 +37,13 @@
     1.4  Note that automated detection from the file-system or search path has
     1.5  been discontinued.  INCOMPATIBILITY.
     1.6  
     1.7 +* Name space: proper configuration options "long_names",
     1.8 +"short_names", "unique_names" instead of former unsynchronized
     1.9 +references.  Minor INCOMPATIBILITY, need to declare options in context
    1.10 +like this:
    1.11 +
    1.12 +  declare [[unique_names = false]]
    1.13 +
    1.14  
    1.15  *** HOL ***
    1.16  
     2.1 --- a/doc-src/Codegen/Thy/Setup.thy	Sat Apr 16 12:46:18 2011 +0200
     2.2 +++ b/doc-src/Codegen/Thy/Setup.thy	Sat Apr 16 13:48:45 2011 +0200
     2.3 @@ -22,6 +22,6 @@
     2.4  
     2.5  setup {* Code_Target.set_default_code_width 74 *}
     2.6  
     2.7 -ML_command {* unique_names := false *}
     2.8 +declare [[unique_names = false]]
     2.9  
    2.10  end
     3.1 --- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Apr 16 12:46:18 2011 +0200
     3.2 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Apr 16 13:48:45 2011 +0200
     3.3 @@ -1112,7 +1112,7 @@
     3.4    @{index_ML Name_Space.declare: "bool -> Name_Space.naming -> binding -> Name_Space.T ->
     3.5    string * Name_Space.T"} \\
     3.6    @{index_ML Name_Space.intern: "Name_Space.T -> string -> string"} \\
     3.7 -  @{index_ML Name_Space.extern: "Name_Space.T -> string -> string"} \\
     3.8 +  @{index_ML Name_Space.extern: "Proof.context -> Name_Space.T -> string -> string"} \\
     3.9    @{index_ML Name_Space.is_concealed: "Name_Space.T -> string -> bool"}
    3.10    \end{mldecls}
    3.11  
    3.12 @@ -1187,7 +1187,7 @@
    3.13    (or their derivatives for @{ML_type theory} and
    3.14    @{ML_type Proof.context}).
    3.15  
    3.16 -  \item @{ML Name_Space.extern}~@{text "space name"} externalizes a
    3.17 +  \item @{ML Name_Space.extern}~@{text "ctxt space name"} externalizes a
    3.18    (fully qualified) internal name.
    3.19  
    3.20    This operation is mostly for printing!  User code should not rely on
     4.1 --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sat Apr 16 12:46:18 2011 +0200
     4.2 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Sat Apr 16 13:48:45 2011 +0200
     4.3 @@ -1610,7 +1610,7 @@
     4.4    \indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: bool -> Name_Space.naming -> binding -> Name_Space.T ->|\isasep\isanewline%
     4.5  \verb|  string * Name_Space.T| \\
     4.6    \indexdef{}{ML}{Name\_Space.intern}\verb|Name_Space.intern: Name_Space.T -> string -> string| \\
     4.7 -  \indexdef{}{ML}{Name\_Space.extern}\verb|Name_Space.extern: Name_Space.T -> string -> string| \\
     4.8 +  \indexdef{}{ML}{Name\_Space.extern}\verb|Name_Space.extern: Proof.context -> Name_Space.T -> string -> string| \\
     4.9    \indexdef{}{ML}{Name\_Space.is\_concealed}\verb|Name_Space.is_concealed: Name_Space.T -> string -> bool|
    4.10    \end{mldecls}
    4.11  
    4.12 @@ -1679,7 +1679,7 @@
    4.13    (or their derivatives for \verb|theory| and
    4.14    \verb|Proof.context|).
    4.15  
    4.16 -  \item \verb|Name_Space.extern|~\isa{space\ name} externalizes a
    4.17 +  \item \verb|Name_Space.extern|~\isa{ctxt\ space\ name} externalizes a
    4.18    (fully qualified) internal name.
    4.19  
    4.20    This operation is mostly for printing!  User code should not rely on
     5.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat Apr 16 12:46:18 2011 +0200
     5.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sat Apr 16 13:48:45 2011 +0200
     5.3 @@ -100,10 +100,10 @@
     5.4      @{index_ML show_sorts: "bool Config.T"} & default @{ML false} \\
     5.5      @{index_ML show_consts: "bool Config.T"} & default @{ML false} \\
     5.6      @{index_ML show_abbrevs: "bool Config.T"} & default @{ML true} \\
     5.7 -    @{index_ML long_names: "bool Unsynchronized.ref"} & default @{ML false} \\
     5.8 -    @{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\
     5.9 -    @{index_ML unique_names: "bool Unsynchronized.ref"} & default @{ML true} \\
    5.10      @{index_ML show_brackets: "bool Config.T"} & default @{ML false} \\
    5.11 +    @{index_ML Name_Space.long_names: "bool Config.T"} & default @{ML false} \\
    5.12 +    @{index_ML Name_Space.short_names: "bool Config.T"} & default @{ML false} \\
    5.13 +    @{index_ML Name_Space.unique_names: "bool Config.T"} & default @{ML true} \\
    5.14      @{index_ML eta_contract: "bool Config.T"} & default @{ML true} \\
    5.15      @{index_ML Goal_Display.goals_limit: "int Config.T"} & default @{ML 10} \\
    5.16      @{index_ML Goal_Display.show_main_goal: "bool Config.T"} & default @{ML false} \\
    5.17 @@ -144,11 +144,6 @@
    5.18  
    5.19    \item @{ML show_abbrevs} controls folding of constant abbreviations.
    5.20  
    5.21 -  \item @{ML long_names}, @{ML short_names}, and @{ML unique_names}
    5.22 -  control the way of printing fully qualified internal names in
    5.23 -  external form.  See also \secref{sec:antiq} for the document
    5.24 -  antiquotation options of the same names.
    5.25 -
    5.26    \item @{ML show_brackets} controls bracketing in pretty printed
    5.27    output.  If set to @{ML true}, all sub-expressions of the pretty
    5.28    printing tree will be parenthesized, even if this produces malformed
    5.29 @@ -156,6 +151,12 @@
    5.30    pretty printed entities may occasionally help to diagnose problems
    5.31    with operator priorities, for example.
    5.32  
    5.33 +  \item @{ML Name_Space.long_names}, @{ML Name_Space.short_names}, and
    5.34 +  @{ML Name_Space.unique_names} control the way of printing fully
    5.35 +  qualified internal names in external form.  See also
    5.36 +  \secref{sec:antiq} for the document antiquotation options of the
    5.37 +  same names.
    5.38 +
    5.39    \item @{ML eta_contract} controls @{text "\<eta>"}-contracted printing of
    5.40    terms.
    5.41  
     6.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat Apr 16 12:46:18 2011 +0200
     6.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sat Apr 16 13:48:45 2011 +0200
     6.3 @@ -122,10 +122,10 @@
     6.4      \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Config.T| & default \verb|false| \\
     6.5      \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & default \verb|false| \\
     6.6      \indexdef{}{ML}{show\_abbrevs}\verb|show_abbrevs: bool Config.T| & default \verb|true| \\
     6.7 -    \indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\
     6.8 -    \indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\
     6.9 -    \indexdef{}{ML}{unique\_names}\verb|unique_names: bool Unsynchronized.ref| & default \verb|true| \\
    6.10      \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool Config.T| & default \verb|false| \\
    6.11 +    \indexdef{}{ML}{Name\_Space.long\_names}\verb|Name_Space.long_names: bool Config.T| & default \verb|false| \\
    6.12 +    \indexdef{}{ML}{Name\_Space.short\_names}\verb|Name_Space.short_names: bool Config.T| & default \verb|false| \\
    6.13 +    \indexdef{}{ML}{Name\_Space.unique\_names}\verb|Name_Space.unique_names: bool Config.T| & default \verb|true| \\
    6.14      \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool Config.T| & default \verb|true| \\
    6.15      \indexdef{}{ML}{Goal\_Display.goals\_limit}\verb|Goal_Display.goals_limit: int Config.T| & default \verb|10| \\
    6.16      \indexdef{}{ML}{Goal\_Display.show\_main\_goal}\verb|Goal_Display.show_main_goal: bool Config.T| & default \verb|false| \\
    6.17 @@ -165,11 +165,6 @@
    6.18  
    6.19    \item \verb|show_abbrevs| controls folding of constant abbreviations.
    6.20  
    6.21 -  \item \verb|long_names|, \verb|short_names|, and \verb|unique_names|
    6.22 -  control the way of printing fully qualified internal names in
    6.23 -  external form.  See also \secref{sec:antiq} for the document
    6.24 -  antiquotation options of the same names.
    6.25 -
    6.26    \item \verb|show_brackets| controls bracketing in pretty printed
    6.27    output.  If set to \verb|true|, all sub-expressions of the pretty
    6.28    printing tree will be parenthesized, even if this produces malformed
    6.29 @@ -177,6 +172,12 @@
    6.30    pretty printed entities may occasionally help to diagnose problems
    6.31    with operator priorities, for example.
    6.32  
    6.33 +  \item \verb|Name_Space.long_names|, \verb|Name_Space.short_names|, and
    6.34 +  \verb|Name_Space.unique_names| control the way of printing fully
    6.35 +  qualified internal names in external form.  See also
    6.36 +  \secref{sec:antiq} for the document antiquotation options of the
    6.37 +  same names.
    6.38 +
    6.39    \item \verb|eta_contract| controls \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-contracted printing of
    6.40    terms.
    6.41  
     7.1 --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Sat Apr 16 12:46:18 2011 +0200
     7.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Sat Apr 16 13:48:45 2011 +0200
     7.3 @@ -152,11 +152,8 @@
     7.4  the qualified name, for example @{text "T.length"}, where @{text T} is the
     7.5  theory it is defined in, to distinguish it from the predefined @{const[source]
     7.6  "List.length"}. In case there is no danger of confusion, you can insist on
     7.7 -short names (no qualifiers) by setting \verb!short_names!, typically
     7.8 -in \texttt{ROOT.ML}:
     7.9 -\begin{quote}
    7.10 -@{ML "short_names := true"}\verb!;!
    7.11 -\end{quote}
    7.12 +short names (no qualifiers) by setting the \verb!short_names!
    7.13 +configuration option in the context.
    7.14  *}
    7.15  
    7.16  subsection {*Variable names\label{sec:varnames}*}
     8.1 --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Sat Apr 16 12:46:18 2011 +0200
     8.2 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Sat Apr 16 13:48:45 2011 +0200
     8.3 @@ -195,11 +195,8 @@
     8.4  If there are multiple declarations of the same name, Isabelle prints
     8.5  the qualified name, for example \isa{T{\isaliteral{2E}{\isachardot}}length}, where \isa{T} is the
     8.6  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
     8.7 -short names (no qualifiers) by setting \verb!short_names!, typically
     8.8 -in \texttt{ROOT.ML}:
     8.9 -\begin{quote}
    8.10 -\verb|short_names := true|\verb!;!
    8.11 -\end{quote}%
    8.12 +short names (no qualifiers) by setting the \verb!short_names!
    8.13 +configuration option in the context.%
    8.14  \end{isamarkuptext}%
    8.15  \isamarkuptrue%
    8.16  %
     9.1 --- a/doc-src/TutorialI/Misc/Itrev.thy	Sat Apr 16 12:46:18 2011 +0200
     9.2 +++ b/doc-src/TutorialI/Misc/Itrev.thy	Sat Apr 16 13:48:45 2011 +0200
     9.3 @@ -2,7 +2,7 @@
     9.4  theory Itrev
     9.5  imports Main
     9.6  begin
     9.7 -ML"unique_names := false"
     9.8 +declare [[unique_names = false]]
     9.9  (*>*)
    9.10  
    9.11  section{*Induction Heuristics*}
    9.12 @@ -141,6 +141,6 @@
    9.13  \index{induction heuristics|)}
    9.14  *}
    9.15  (*<*)
    9.16 -ML"unique_names := true"
    9.17 +declare [[unique_names = true]]
    9.18  end
    9.19  (*>*)
    10.1 --- a/doc-src/TutorialI/Misc/document/Itrev.tex	Sat Apr 16 12:46:18 2011 +0200
    10.2 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex	Sat Apr 16 13:48:45 2011 +0200
    10.3 @@ -15,19 +15,6 @@
    10.4  %
    10.5  \endisadelimtheory
    10.6  %
    10.7 -\isadelimML
    10.8 -%
    10.9 -\endisadelimML
   10.10 -%
   10.11 -\isatagML
   10.12 -%
   10.13 -\endisatagML
   10.14 -{\isafoldML}%
   10.15 -%
   10.16 -\isadelimML
   10.17 -%
   10.18 -\endisadelimML
   10.19 -%
   10.20  \isamarkupsection{Induction Heuristics%
   10.21  }
   10.22  \isamarkuptrue%
   10.23 @@ -216,19 +203,6 @@
   10.24  \end{isamarkuptext}%
   10.25  \isamarkuptrue%
   10.26  %
   10.27 -\isadelimML
   10.28 -%
   10.29 -\endisadelimML
   10.30 -%
   10.31 -\isatagML
   10.32 -%
   10.33 -\endisatagML
   10.34 -{\isafoldML}%
   10.35 -%
   10.36 -\isadelimML
   10.37 -%
   10.38 -\endisadelimML
   10.39 -%
   10.40  \isadelimtheory
   10.41  %
   10.42  \endisadelimtheory
    11.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Apr 16 12:46:18 2011 +0200
    11.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Sat Apr 16 13:48:45 2011 +0200
    11.3 @@ -848,8 +848,8 @@
    11.4                              th |> backquote_thm
    11.5                            else
    11.6                              let
    11.7 -                              val name1 = Facts.extern facts name0
    11.8 -                              val name2 = Name_Space.extern full_space name0
    11.9 +                              val name1 = Facts.extern ctxt facts name0
   11.10 +                              val name2 = Name_Space.extern ctxt full_space name0
   11.11                              in
   11.12                                case find_first check_thms [name1, name2, name0] of
   11.13                                  SOME name => make_name reserved multi j name
    12.1 --- a/src/HOL/Tools/inductive.ML	Sat Apr 16 12:46:18 2011 +0200
    12.2 +++ b/src/HOL/Tools/inductive.ML	Sat Apr 16 13:48:45 2011 +0200
    12.3 @@ -151,7 +151,7 @@
    12.4      val (tab, monos) = get_inductives ctxt;
    12.5      val space = Consts.space_of (ProofContext.consts_of ctxt);
    12.6    in
    12.7 -    [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table (space, tab))),
    12.8 +    [Pretty.strs ("(co)inductives:" :: map #1 (Name_Space.extern_table ctxt (space, tab))),
    12.9       Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm ctxt) monos)]
   12.10      |> Pretty.chunks |> Pretty.writeln
   12.11    end;
    13.1 --- a/src/HOL/Tools/record.ML	Sat Apr 16 12:46:18 2011 +0200
    13.2 +++ b/src/HOL/Tools/record.ML	Sat Apr 16 13:48:45 2011 +0200
    13.3 @@ -914,7 +914,7 @@
    13.4  fun record_tr' ctxt t =
    13.5    let
    13.6      val thy = ProofContext.theory_of ctxt;
    13.7 -    val extern = Consts.extern (ProofContext.consts_of ctxt);
    13.8 +    val extern = Consts.extern ctxt (ProofContext.consts_of ctxt);
    13.9  
   13.10      fun strip_fields t =
   13.11        (case strip_comb t of
   13.12 @@ -957,7 +957,7 @@
   13.13  
   13.14  fun dest_update ctxt c =
   13.15    (case try Lexicon.unmark_const c of
   13.16 -    SOME d => try (unsuffix updateN) (Consts.extern (ProofContext.consts_of ctxt) d)
   13.17 +    SOME d => try (unsuffix updateN) (Consts.extern ctxt (ProofContext.consts_of ctxt) d)
   13.18    | NONE => NONE);
   13.19  
   13.20  fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
    14.1 --- a/src/Pure/General/name_space.ML	Sat Apr 16 12:46:18 2011 +0200
    14.2 +++ b/src/Pure/General/name_space.ML	Sat Apr 16 13:48:45 2011 +0200
    14.3 @@ -7,16 +7,8 @@
    14.4  
    14.5  type xstring = string;    (*external names*)
    14.6  
    14.7 -signature BASIC_NAME_SPACE =
    14.8 -sig
    14.9 -  val long_names: bool Unsynchronized.ref
   14.10 -  val short_names: bool Unsynchronized.ref
   14.11 -  val unique_names: bool Unsynchronized.ref
   14.12 -end;
   14.13 -
   14.14  signature NAME_SPACE =
   14.15  sig
   14.16 -  include BASIC_NAME_SPACE
   14.17    val hidden: string -> string
   14.18    val is_hidden: string -> bool
   14.19    type T
   14.20 @@ -27,9 +19,16 @@
   14.21    val markup_entry: T -> string -> Markup.T
   14.22    val is_concealed: T -> string -> bool
   14.23    val intern: T -> xstring -> string
   14.24 -  val extern_flags: {long_names: bool, short_names: bool, unique_names: bool} ->
   14.25 -    T -> string -> xstring
   14.26 -  val extern: T -> string -> xstring
   14.27 +  val long_names_default: bool Unsynchronized.ref
   14.28 +  val long_names_raw: Config.raw
   14.29 +  val long_names: bool Config.T
   14.30 +  val short_names_default: bool Unsynchronized.ref
   14.31 +  val short_names_raw: Config.raw
   14.32 +  val short_names: bool Config.T
   14.33 +  val unique_names_default: bool Unsynchronized.ref
   14.34 +  val unique_names_raw: Config.raw
   14.35 +  val unique_names: bool Config.T
   14.36 +  val extern: Proof.context -> T -> string -> xstring
   14.37    val hide: bool -> string -> T -> T
   14.38    val merge: T * T -> T
   14.39    type naming
   14.40 @@ -55,8 +54,8 @@
   14.41    val merge_tables: 'a table * 'a table -> 'a table
   14.42    val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
   14.43      'a table * 'a table -> 'a table
   14.44 -  val dest_table: 'a table -> (string * 'a) list
   14.45 -  val extern_table: 'a table -> (xstring * 'a) list
   14.46 +  val dest_table: Proof.context -> 'a table -> (string * 'a) list
   14.47 +  val extern_table: Proof.context -> 'a table -> (xstring * 'a) list
   14.48  end;
   14.49  
   14.50  structure Name_Space: NAME_SPACE =
   14.51 @@ -154,8 +153,25 @@
   14.52  
   14.53  fun intern space xname = #1 (lookup space xname);
   14.54  
   14.55 -fun extern_flags {long_names, short_names, unique_names} space name =
   14.56 +
   14.57 +val long_names_default = Unsynchronized.ref false;
   14.58 +val long_names_raw = Config.declare "long_names" (fn _ => Config.Bool (! long_names_default));
   14.59 +val long_names = Config.bool long_names_raw;
   14.60 +
   14.61 +val short_names_default = Unsynchronized.ref false;
   14.62 +val short_names_raw = Config.declare "short_names" (fn _ => Config.Bool (! short_names_default));
   14.63 +val short_names = Config.bool short_names_raw;
   14.64 +
   14.65 +val unique_names_default = Unsynchronized.ref true;
   14.66 +val unique_names_raw = Config.declare "unique_names" (fn _ => Config.Bool (! unique_names_default));
   14.67 +val unique_names = Config.bool unique_names_raw;
   14.68 +
   14.69 +fun extern ctxt space name =
   14.70    let
   14.71 +    val long_names = Config.get ctxt long_names;
   14.72 +    val short_names = Config.get ctxt short_names;
   14.73 +    val unique_names = Config.get ctxt unique_names;
   14.74 +
   14.75      fun valid require_unique xname =
   14.76        let val (name', is_unique) = lookup space xname
   14.77        in name = name' andalso (not require_unique orelse is_unique) end;
   14.78 @@ -168,16 +184,6 @@
   14.79      else ext (get_accesses space name)
   14.80    end;
   14.81  
   14.82 -val long_names = Unsynchronized.ref false;
   14.83 -val short_names = Unsynchronized.ref false;
   14.84 -val unique_names = Unsynchronized.ref true;
   14.85 -
   14.86 -fun extern space name =
   14.87 -  extern_flags
   14.88 -   {long_names = ! long_names,
   14.89 -    short_names = ! short_names,
   14.90 -    unique_names = ! unique_names} space name;
   14.91 -
   14.92  
   14.93  (* modify internals *)
   14.94  
   14.95 @@ -385,15 +391,12 @@
   14.96  fun join_tables f ((space1, tab1), (space2, tab2)) =
   14.97    (merge (space1, space2), Symtab.join f (tab1, tab2));
   14.98  
   14.99 -fun ext_table (space, tab) =
  14.100 -  Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
  14.101 +fun ext_table ctxt (space, tab) =
  14.102 +  Symtab.fold (fn (name, x) => cons ((name, extern ctxt space name), x)) tab []
  14.103    |> Library.sort_wrt (#2 o #1);
  14.104  
  14.105 -fun dest_table tab = map (apfst #1) (ext_table tab);
  14.106 -fun extern_table tab = map (apfst #2) (ext_table tab);
  14.107 +fun dest_table ctxt tab = map (apfst #1) (ext_table ctxt tab);
  14.108 +fun extern_table ctxt tab = map (apfst #2) (ext_table ctxt tab);
  14.109  
  14.110  end;
  14.111  
  14.112 -structure Basic_Name_Space: BASIC_NAME_SPACE = Name_Space;
  14.113 -open Basic_Name_Space;
  14.114 -
    15.1 --- a/src/Pure/Isar/attrib.ML	Sat Apr 16 12:46:18 2011 +0200
    15.2 +++ b/src/Pure/Isar/attrib.ML	Sat Apr 16 13:48:45 2011 +0200
    15.3 @@ -73,11 +73,12 @@
    15.4  
    15.5  fun print_attributes thy =
    15.6    let
    15.7 +    val ctxt = ProofContext.init_global thy;
    15.8      val attribs = Attributes.get thy;
    15.9      fun prt_attr (name, (_, comment)) = Pretty.block
   15.10        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   15.11    in
   15.12 -    [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table attribs))]
   15.13 +    [Pretty.big_list "attributes:" (map prt_attr (Name_Space.extern_table ctxt attribs))]
   15.14      |> Pretty.chunks |> Pretty.writeln
   15.15    end;
   15.16  
   15.17 @@ -90,7 +91,7 @@
   15.18  val intern = Name_Space.intern o #1 o Attributes.get;
   15.19  val intern_src = Args.map_name o intern;
   15.20  
   15.21 -val extern = Name_Space.extern o #1 o Attributes.get o ProofContext.theory_of;
   15.22 +fun extern ctxt = Name_Space.extern ctxt (#1 (Attributes.get (ProofContext.theory_of ctxt)));
   15.23  
   15.24  
   15.25  (* pretty printing *)
   15.26 @@ -341,7 +342,7 @@
   15.27          Pretty.block [Pretty.str (name ^ ": " ^ Config.print_type value ^ " ="), Pretty.brk 1,
   15.28            Pretty.str (Config.print_value value)]
   15.29        end;
   15.30 -    val configs = Name_Space.extern_table (#1 (Attributes.get thy), Configs.get thy);
   15.31 +    val configs = Name_Space.extern_table ctxt (#1 (Attributes.get thy), Configs.get thy);
   15.32    in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
   15.33  
   15.34  
   15.35 @@ -408,6 +409,9 @@
   15.36    register_config Printer.show_question_marks_raw #>
   15.37    register_config Syntax.ambiguity_level_raw #>
   15.38    register_config Syntax_Trans.eta_contract_raw #>
   15.39 +  register_config Name_Space.long_names_raw #>
   15.40 +  register_config Name_Space.short_names_raw #>
   15.41 +  register_config Name_Space.unique_names_raw #>
   15.42    register_config ML_Context.trace_raw #>
   15.43    register_config ProofContext.show_abbrevs_raw #>
   15.44    register_config Goal_Display.goals_limit_raw #>
    16.1 --- a/src/Pure/Isar/expression.ML	Sat Apr 16 12:46:18 2011 +0200
    16.2 +++ b/src/Pure/Isar/expression.ML	Sat Apr 16 13:48:45 2011 +0200
    16.3 @@ -616,7 +616,7 @@
    16.4  fun aprop_tr' n c = (Lexicon.mark_const c, fn ctxt => fn args =>
    16.5    if length args = n then
    16.6      Syntax.const "_aprop" $   (* FIXME avoid old-style early externing (!??) *)
    16.7 -      Term.list_comb (Syntax.free (Consts.extern (ProofContext.consts_of ctxt) c), args)
    16.8 +      Term.list_comb (Syntax.free (Consts.extern ctxt (ProofContext.consts_of ctxt) c), args)
    16.9    else raise Match);
   16.10  
   16.11  (* define one predicate including its intro rule and axioms
    17.1 --- a/src/Pure/Isar/isar_cmd.ML	Sat Apr 16 12:46:18 2011 +0200
    17.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Apr 16 13:48:45 2011 +0200
    17.3 @@ -399,11 +399,11 @@
    17.4  
    17.5  val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
    17.6    let
    17.7 -    val thy = Toplevel.theory_of state;
    17.8 -    val {classes = (space, algebra), ...} = Type.rep_tsig (Sign.tsig_of thy);
    17.9 +    val ctxt = Toplevel.context_of state;
   17.10 +    val {classes = (space, algebra), ...} = Type.rep_tsig (ProofContext.tsig_of ctxt);
   17.11      val classes = Sorts.classes_of algebra;
   17.12      fun entry (c, (i, (_, cs))) =
   17.13 -      (i, {name = Name_Space.extern space c, ID = c, parents = cs,
   17.14 +      (i, {name = Name_Space.extern ctxt space c, ID = c, parents = cs,
   17.15              dir = "", unfold = true, path = ""});
   17.16      val gr =
   17.17        Graph.fold (cons o entry) classes []
    18.1 --- a/src/Pure/Isar/locale.ML	Sat Apr 16 12:46:18 2011 +0200
    18.2 +++ b/src/Pure/Isar/locale.ML	Sat Apr 16 13:48:45 2011 +0200
    18.3 @@ -162,7 +162,7 @@
    18.4  );
    18.5  
    18.6  val intern = Name_Space.intern o #1 o Locales.get;
    18.7 -val extern = Name_Space.extern o #1 o Locales.get;
    18.8 +fun extern thy = Name_Space.extern (ProofContext.init_global thy) (#1 (Locales.get thy));
    18.9  
   18.10  val get_locale = Symtab.lookup o #2 o Locales.get;
   18.11  val defined = Symtab.defined o #2 o Locales.get;
   18.12 @@ -630,7 +630,8 @@
   18.13  val all_locales = Symtab.keys o snd o Locales.get;
   18.14  
   18.15  fun print_locales thy =
   18.16 -  Pretty.strs ("locales:" :: map #1 (Name_Space.extern_table (Locales.get thy)))
   18.17 +  Pretty.strs ("locales:" ::
   18.18 +    map #1 (Name_Space.extern_table (ProofContext.init_global thy) (Locales.get thy)))
   18.19    |> Pretty.writeln;
   18.20  
   18.21  fun print_locale thy show_facts raw_name =
    19.1 --- a/src/Pure/Isar/method.ML	Sat Apr 16 12:46:18 2011 +0200
    19.2 +++ b/src/Pure/Isar/method.ML	Sat Apr 16 13:48:45 2011 +0200
    19.3 @@ -334,11 +334,12 @@
    19.4  
    19.5  fun print_methods thy =
    19.6    let
    19.7 +    val ctxt = ProofContext.init_global thy;
    19.8      val meths = Methods.get thy;
    19.9      fun prt_meth (name, (_, comment)) = Pretty.block
   19.10        [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   19.11    in
   19.12 -    [Pretty.big_list "methods:" (map prt_meth (Name_Space.extern_table meths))]
   19.13 +    [Pretty.big_list "methods:" (map prt_meth (Name_Space.extern_table ctxt meths))]
   19.14      |> Pretty.chunks |> Pretty.writeln
   19.15    end;
   19.16  
    20.1 --- a/src/Pure/Isar/proof_context.ML	Sat Apr 16 12:46:18 2011 +0200
    20.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Apr 16 13:48:45 2011 +0200
    20.3 @@ -304,8 +304,8 @@
    20.4      val global_facts = Global_Theory.facts_of (theory_of ctxt);
    20.5    in
    20.6      if is_some (Facts.lookup (Context.Proof ctxt) local_facts name)
    20.7 -    then Facts.extern local_facts name
    20.8 -    else Facts.extern global_facts name
    20.9 +    then Facts.extern ctxt local_facts name
   20.10 +    else Facts.extern ctxt global_facts name
   20.11    end;
   20.12  
   20.13  
   20.14 @@ -1152,7 +1152,8 @@
   20.15        | add_abbr (c, (T, SOME t)) =
   20.16            if not show_globals andalso Symtab.defined globals c then I
   20.17            else cons (c, Logic.mk_equals (Const (c, T), t));
   20.18 -    val abbrevs = Name_Space.extern_table (space, Symtab.make (Symtab.fold add_abbr consts []));
   20.19 +    val abbrevs =
   20.20 +      Name_Space.extern_table ctxt (space, Symtab.make (Symtab.fold add_abbr consts []));
   20.21    in
   20.22      if null abbrevs then []
   20.23      else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
    21.1 --- a/src/Pure/ProofGeneral/preferences.ML	Sat Apr 16 12:46:18 2011 +0200
    21.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Sat Apr 16 13:48:45 2011 +0200
    21.3 @@ -124,7 +124,7 @@
    21.4    bool_pref Goal_Display.show_consts_default
    21.5      "show-consts"
    21.6      "Show types of consts in Isabelle goal display",
    21.7 -  bool_pref long_names
    21.8 +  bool_pref Name_Space.long_names_default
    21.9      "long-names"
   21.10      "Show fully qualified names in Isabelle terms",
   21.11    bool_pref Printer.show_brackets_default
    22.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Apr 16 12:46:18 2011 +0200
    22.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Apr 16 13:48:45 2011 +0200
    22.3 @@ -517,12 +517,15 @@
    22.4  
    22.5  local
    22.6  
    22.7 -fun theory_facts name =
    22.8 +fun theory_facts thy =
    22.9 +  (map Global_Theory.facts_of (Theory.parents_of thy), Global_Theory.facts_of thy);
   22.10 +
   22.11 +fun thms_of_thy name =
   22.12    let val thy = Thy_Info.get_theory name
   22.13 -  in (map Global_Theory.facts_of (Theory.parents_of thy), Global_Theory.facts_of thy) end;
   22.14 +  in map fst (theory_facts thy |-> Facts.extern_static (ProofContext.init_global thy)) end;
   22.15  
   22.16 -fun thms_of_thy name = map fst (theory_facts name |-> Facts.extern_static);
   22.17 -fun qualified_thms_of_thy name = map fst (theory_facts name |-> Facts.dest_static);
   22.18 +fun qualified_thms_of_thy name =
   22.19 +  map fst (theory_facts (Thy_Info.get_theory name) |-> Facts.dest_static);
   22.20  
   22.21  in
   22.22  
    23.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sat Apr 16 12:46:18 2011 +0200
    23.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sat Apr 16 13:48:45 2011 +0200
    23.3 @@ -605,6 +605,8 @@
    23.4  fun unparse_t t_to_ast prt_t markup ctxt t =
    23.5    let
    23.6      val syn = ProofContext.syn_of ctxt;
    23.7 +    val tsig = ProofContext.tsig_of ctxt;
    23.8 +    val consts = ProofContext.consts_of ctxt;
    23.9  
   23.10      fun token_trans "_tfree" x = SOME (Pretty.mark_str (Markup.tfree, x))
   23.11        | token_trans "_tvar" x = SOME (Pretty.mark_str (Markup.tvar, x))
   23.12 @@ -620,9 +622,9 @@
   23.13          SOME "" => ([], c)
   23.14        | SOME b => markup_extern b
   23.15        | NONE => c |> Lexicon.unmark
   23.16 -         {case_class = fn x => ([Markup.tclass x], Type.extern_class (ProofContext.tsig_of ctxt) x),
   23.17 -          case_type = fn x => ([Markup.tycon x], Type.extern_type (ProofContext.tsig_of ctxt) x),
   23.18 -          case_const = fn x => ([Markup.const x], Consts.extern (ProofContext.consts_of ctxt) x),
   23.19 +         {case_class = fn x => ([Markup.tclass x], Type.extern_class ctxt tsig x),
   23.20 +          case_type = fn x => ([Markup.tycon x], Type.extern_type ctxt tsig x),
   23.21 +          case_const = fn x => ([Markup.const x], Consts.extern ctxt consts x),
   23.22            case_fixed = fn x => free_or_skolem ctxt x,
   23.23            case_default = fn x => ([], x)});
   23.24    in
    24.1 --- a/src/Pure/Thy/thy_output.ML	Sat Apr 16 12:46:18 2011 +0200
    24.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Apr 16 13:48:45 2011 +0200
    24.3 @@ -450,9 +450,9 @@
    24.4  val _ = add_option "show_structs" (Config.put show_structs o boolean);
    24.5  val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
    24.6  val _ = add_option "show_abbrevs" (Config.put show_abbrevs o boolean);
    24.7 -val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
    24.8 -val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);
    24.9 -val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);
   24.10 +val _ = add_option "long_names" (Config.put Name_Space.long_names o boolean);
   24.11 +val _ = add_option "short_names" (Config.put Name_Space.short_names o boolean);
   24.12 +val _ = add_option "unique_names" (Config.put Name_Space.unique_names o boolean);
   24.13  val _ = add_option "eta_contract" (Config.put Syntax_Trans.eta_contract o boolean);
   24.14  val _ = add_option "display" (Config.put display o boolean);
   24.15  val _ = add_option "break" (Config.put break o boolean);
   24.16 @@ -510,11 +510,11 @@
   24.17    in ProofContext.pretty_term_abbrev ctxt' eq end;
   24.18  
   24.19  fun pretty_class ctxt =
   24.20 -  Pretty.str o Type.extern_class (ProofContext.tsig_of ctxt) o ProofContext.read_class ctxt;
   24.21 +  Pretty.str o Type.extern_class ctxt (ProofContext.tsig_of ctxt) o ProofContext.read_class ctxt;
   24.22  
   24.23  fun pretty_type ctxt s =
   24.24    let val Type (name, _) = ProofContext.read_type_name_proper ctxt false s
   24.25 -  in Pretty.str (Type.extern_type (ProofContext.tsig_of ctxt) name) end;
   24.26 +  in Pretty.str (Type.extern_type ctxt (ProofContext.tsig_of ctxt) name) end;
   24.27  
   24.28  fun pretty_prf full ctxt = Proof_Syntax.pretty_proof_of ctxt full;
   24.29  
    25.1 --- a/src/Pure/Tools/find_theorems.ML	Sat Apr 16 12:46:18 2011 +0200
    25.2 +++ b/src/Pure/Tools/find_theorems.ML	Sat Apr 16 13:48:45 2011 +0200
    25.3 @@ -381,8 +381,11 @@
    25.4      val space = Facts.space_of (Global_Theory.facts_of (ProofContext.theory_of ctxt));
    25.5  
    25.6      val shorten =
    25.7 -      Name_Space.extern_flags
    25.8 -        {long_names = false, short_names = false, unique_names = false} space;
    25.9 +      Name_Space.extern
   25.10 +        (ctxt
   25.11 +          |> Config.put Name_Space.long_names false
   25.12 +          |> Config.put Name_Space.short_names false
   25.13 +          |> Config.put Name_Space.unique_names false) space;
   25.14  
   25.15      fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
   25.16            nicer_name (shorten x, i) (shorten y, j)
    26.1 --- a/src/Pure/consts.ML	Sat Apr 16 12:46:18 2011 +0200
    26.2 +++ b/src/Pure/consts.ML	Sat Apr 16 13:48:45 2011 +0200
    26.3 @@ -22,9 +22,9 @@
    26.4    val alias: Name_Space.naming -> binding -> string -> T -> T
    26.5    val is_concealed: T -> string -> bool
    26.6    val intern: T -> xstring -> string
    26.7 -  val extern: T -> string -> xstring
    26.8 +  val extern: Proof.context -> T -> string -> xstring
    26.9    val intern_syntax: T -> xstring -> string
   26.10 -  val extern_syntax: T -> string -> xstring
   26.11 +  val extern_syntax: Proof.context -> T -> string -> xstring
   26.12    val read_const: T -> string -> term
   26.13    val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term  (*exception TYPE*)
   26.14    val typargs: T -> string * typ -> typ list
   26.15 @@ -129,16 +129,16 @@
   26.16  val is_concealed = Name_Space.is_concealed o space_of;
   26.17  
   26.18  val intern = Name_Space.intern o space_of;
   26.19 -val extern = Name_Space.extern o space_of;
   26.20 +fun extern ctxt = Name_Space.extern ctxt o space_of;
   26.21  
   26.22  fun intern_syntax consts s =
   26.23    (case try Lexicon.unmark_const s of
   26.24      SOME c => c
   26.25    | NONE => intern consts s);
   26.26  
   26.27 -fun extern_syntax consts s =
   26.28 +fun extern_syntax ctxt consts s =
   26.29    (case try Lexicon.unmark_const s of
   26.30 -    SOME c => extern consts c
   26.31 +    SOME c => extern ctxt consts c
   26.32    | NONE => s);
   26.33  
   26.34  
    27.1 --- a/src/Pure/display.ML	Sat Apr 16 12:46:18 2011 +0200
    27.2 +++ b/src/Pure/display.ML	Sat Apr 16 13:48:45 2011 +0200
    27.3 @@ -187,25 +187,25 @@
    27.4      val {restricts, reducts} = Defs.dest defs;
    27.5      val {naming = _, syn = _, tsig, consts} = Sign.rep_sg thy;
    27.6      val {constants, constraints} = Consts.dest consts;
    27.7 -    val extern_const = Name_Space.extern (#1 constants);
    27.8 +    val extern_const = Name_Space.extern ctxt (#1 constants);
    27.9      val {classes, default, types, ...} = Type.rep_tsig tsig;
   27.10      val (class_space, class_algebra) = classes;
   27.11      val classes = Sorts.classes_of class_algebra;
   27.12      val arities = Sorts.arities_of class_algebra;
   27.13  
   27.14 -    val clsses = Name_Space.dest_table (class_space, Symtab.make (Graph.dest classes));
   27.15 -    val tdecls = Name_Space.dest_table types;
   27.16 -    val arties = Name_Space.dest_table (Sign.type_space thy, arities);
   27.17 +    val clsses = Name_Space.dest_table ctxt (class_space, Symtab.make (Graph.dest classes));
   27.18 +    val tdecls = Name_Space.dest_table ctxt types;
   27.19 +    val arties = Name_Space.dest_table ctxt (Sign.type_space thy, arities);
   27.20  
   27.21      fun prune_const c = not verbose andalso Consts.is_concealed consts c;
   27.22 -    val cnsts = Name_Space.extern_table (#1 constants,
   27.23 +    val cnsts = Name_Space.extern_table ctxt (#1 constants,
   27.24        Symtab.make (filter_out (prune_const o fst) (Symtab.dest (#2 constants))));
   27.25  
   27.26      val log_cnsts = map_filter (fn (c, (ty, NONE)) => SOME (c, ty) | _ => NONE) cnsts;
   27.27      val abbrevs = map_filter (fn (c, (ty, SOME t)) => SOME (c, (ty, t)) | _ => NONE) cnsts;
   27.28 -    val cnstrs = Name_Space.extern_table constraints;
   27.29 +    val cnstrs = Name_Space.extern_table ctxt constraints;
   27.30  
   27.31 -    val axms = Name_Space.extern_table axioms;
   27.32 +    val axms = Name_Space.extern_table ctxt axioms;
   27.33  
   27.34      val (reds0, (reds1, reds2)) = filter_out (prune_const o fst o fst) reducts
   27.35        |> map (fn (lhs, rhs) =>
   27.36 @@ -225,7 +225,7 @@
   27.37        Pretty.big_list "abbreviations:" (map pretty_abbrev abbrevs),
   27.38        Pretty.big_list "constraints:" (map (Pretty.block o prt_const) cnstrs),
   27.39        Pretty.big_list "axioms:" (map pretty_axm axms),
   27.40 -      Pretty.strs ("oracles:" :: Thm.extern_oracles thy),
   27.41 +      Pretty.strs ("oracles:" :: Thm.extern_oracles ctxt),
   27.42        Pretty.big_list "definitions:"
   27.43          [pretty_finals reds0,
   27.44           Pretty.big_list "non-overloaded:" (map pretty_reduct reds1),
    28.1 --- a/src/Pure/facts.ML	Sat Apr 16 12:46:18 2011 +0200
    28.2 +++ b/src/Pure/facts.ML	Sat Apr 16 13:48:45 2011 +0200
    28.3 @@ -23,12 +23,12 @@
    28.4    val space_of: T -> Name_Space.T
    28.5    val is_concealed: T -> string -> bool
    28.6    val intern: T -> xstring -> string
    28.7 -  val extern: T -> string -> xstring
    28.8 +  val extern: Proof.context -> T -> string -> xstring
    28.9    val lookup: Context.generic -> T -> string -> (bool * thm list) option
   28.10    val defined: T -> string -> bool
   28.11    val fold_static: (string * thm list -> 'a -> 'a) -> T -> 'a -> 'a
   28.12    val dest_static: T list -> T -> (string * thm list) list
   28.13 -  val extern_static: T list -> T -> (xstring * thm list) list
   28.14 +  val extern_static: Proof.context -> T list -> T -> (xstring * thm list) list
   28.15    val props: T -> thm list
   28.16    val could_unify: T -> term -> thm list
   28.17    val merge: T * T -> T
   28.18 @@ -141,7 +141,7 @@
   28.19  val is_concealed = Name_Space.is_concealed o space_of;
   28.20  
   28.21  val intern = Name_Space.intern o space_of;
   28.22 -val extern = Name_Space.extern o space_of;
   28.23 +fun extern ctxt = Name_Space.extern ctxt o space_of;
   28.24  
   28.25  val defined = Symtab.defined o table_of;
   28.26  
   28.27 @@ -165,8 +165,8 @@
   28.28  fun dest_static prev_facts facts =
   28.29    sort_wrt #1 (diff_table prev_facts facts);
   28.30  
   28.31 -fun extern_static prev_facts facts =
   28.32 -  sort_wrt #1 (diff_table prev_facts facts |> map (apfst (extern facts)));
   28.33 +fun extern_static ctxt prev_facts facts =
   28.34 +  sort_wrt #1 (diff_table prev_facts facts |> map (apfst (extern ctxt facts)));
   28.35  
   28.36  
   28.37  (* indexed props *)
    29.1 --- a/src/Pure/sign.ML	Sat Apr 16 12:46:18 2011 +0200
    29.2 +++ b/src/Pure/sign.ML	Sat Apr 16 13:48:45 2011 +0200
    29.3 @@ -233,11 +233,11 @@
    29.4  fun const_alias b c thy = map_consts (Consts.alias (naming_of thy) b c) thy;
    29.5  
    29.6  val intern_class = Name_Space.intern o class_space;
    29.7 -val extern_class = Name_Space.extern o class_space;
    29.8 +fun extern_class thy = Name_Space.extern (ProofContext.init_global thy) (class_space thy);
    29.9  val intern_type = Name_Space.intern o type_space;
   29.10 -val extern_type = Name_Space.extern o type_space;
   29.11 +fun extern_type thy = Name_Space.extern (ProofContext.init_global thy) (type_space thy);
   29.12  val intern_const = Name_Space.intern o const_space;
   29.13 -val extern_const = Name_Space.extern o const_space;
   29.14 +fun extern_const thy = Name_Space.extern (ProofContext.init_global thy) (const_space thy);
   29.15  
   29.16  
   29.17  
    30.1 --- a/src/Pure/thm.ML	Sat Apr 16 12:46:18 2011 +0200
    30.2 +++ b/src/Pure/thm.ML	Sat Apr 16 13:48:45 2011 +0200
    30.3 @@ -147,7 +147,7 @@
    30.4    val compose_no_flatten: bool -> thm * int -> int -> thm -> thm Seq.seq
    30.5    val bicompose: bool -> bool * thm * int -> int -> thm -> thm Seq.seq
    30.6    val biresolution: bool -> (bool * thm) list -> int -> thm -> thm Seq.seq
    30.7 -  val extern_oracles: theory -> xstring list
    30.8 +  val extern_oracles: Proof.context -> xstring list
    30.9    val add_oracle: binding * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory
   30.10  end;
   30.11  
   30.12 @@ -1734,7 +1734,8 @@
   30.13    fun merge data : T = Name_Space.merge_tables data;
   30.14  );
   30.15  
   30.16 -val extern_oracles = map #1 o Name_Space.extern_table o Oracles.get;
   30.17 +fun extern_oracles ctxt =
   30.18 +  map #1 (Name_Space.extern_table ctxt (Oracles.get (ProofContext.theory_of ctxt)));
   30.19  
   30.20  fun add_oracle (b, oracle) thy =
   30.21    let
    31.1 --- a/src/Pure/type.ML	Sat Apr 16 12:46:18 2011 +0200
    31.2 +++ b/src/Pure/type.ML	Sat Apr 16 13:48:45 2011 +0200
    31.3 @@ -28,7 +28,7 @@
    31.4    val class_space: tsig -> Name_Space.T
    31.5    val class_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
    31.6    val intern_class: tsig -> xstring -> string
    31.7 -  val extern_class: tsig -> string -> xstring
    31.8 +  val extern_class: Proof.context -> tsig -> string -> xstring
    31.9    val defaultS: tsig -> sort
   31.10    val logical_types: tsig -> string list
   31.11    val eq_sort: tsig -> sort * sort -> bool
   31.12 @@ -49,7 +49,7 @@
   31.13    val type_space: tsig -> Name_Space.T
   31.14    val type_alias: Name_Space.naming -> binding -> string -> tsig -> tsig
   31.15    val intern_type: tsig -> xstring -> string
   31.16 -  val extern_type: tsig -> string -> xstring
   31.17 +  val extern_type: Proof.context -> tsig -> string -> xstring
   31.18    val is_logtype: tsig -> string -> bool
   31.19    val the_decl: tsig -> string -> decl
   31.20    val cert_typ_mode: mode -> tsig -> typ -> typ
   31.21 @@ -192,7 +192,7 @@
   31.22    ((Name_Space.alias naming binding name space, classes), default, types));
   31.23  
   31.24  val intern_class = Name_Space.intern o class_space;
   31.25 -val extern_class = Name_Space.extern o class_space;
   31.26 +fun extern_class ctxt = Name_Space.extern ctxt o class_space;
   31.27  
   31.28  fun defaultS (TSig {default, ...}) = default;
   31.29  fun logical_types (TSig {log_types, ...}) = log_types;
   31.30 @@ -237,7 +237,7 @@
   31.31    (classes, default, (Name_Space.alias naming binding name space, types)));
   31.32  
   31.33  val intern_type = Name_Space.intern o type_space;
   31.34 -val extern_type = Name_Space.extern o type_space;
   31.35 +fun extern_type ctxt = Name_Space.extern ctxt o type_space;
   31.36  
   31.37  val is_logtype = member (op =) o logical_types;
   31.38