modernized some structure names, keeping a few legacy aliases;
authorwenzelm
Mon May 31 21:06:57 2010 +0200 (2010-05-31)
changeset 372163165bc303f66
parent 37215 91dfe7dccfdf
child 37217 b2769ba027b0
modernized some structure names, keeping a few legacy aliases;
NEWS
doc-src/Classes/Thy/document/Classes.tex
doc-src/IsarImplementation/Thy/Integration.thy
doc-src/IsarImplementation/Thy/document/Integration.tex
doc-src/IsarRef/Thy/ROOT-HOLCF.ML
doc-src/IsarRef/Thy/ROOT-ZF.ML
doc-src/IsarRef/Thy/ROOT.ML
doc-src/Main/Docs/Main_Doc.thy
doc-src/System/Thy/ROOT.ML
doc-src/TutorialI/Rules/Primes.thy
doc-src/TutorialI/Types/Numbers.thy
doc-src/TutorialI/Types/document/Numbers.tex
doc-src/TutorialI/Types/document/Pairs.tex
doc-src/TutorialI/settings.ML
doc-src/antiquote_setup.ML
doc-src/more_antiquote.ML
doc-src/rail.ML
src/HOL/Tools/ATP_Manager/atp_manager.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/simple_thread.ML
src/Pure/Concurrent/single_assignment.ML
src/Pure/Concurrent/synchronized.ML
src/Pure/Concurrent/task_queue.ML
src/Pure/General/scan.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_document.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/method.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/toplevel.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/ML/ml_thms.ML
src/Pure/ProofGeneral/pgip_isabelle.ML
src/Pure/ProofGeneral/pgip_parser.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
src/Pure/ROOT.ML
src/Pure/Syntax/mixfix.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syn_trans.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/type_ext.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/isar.ML
src/Pure/System/session.ML
src/Pure/Thy/present.ML
src/Pure/Thy/thm_deps.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
src/Pure/Thy/thy_output.ML
src/Pure/Thy/thy_syntax.ML
src/Pure/context.ML
src/Pure/morphism.ML
src/Pure/proofterm.ML
src/Pure/pure_setup.ML
src/Pure/pure_thy.ML
src/Pure/simplifier.ML
src/Tools/Code/code_eval.ML
src/Tools/Code/code_thingol.ML
src/Tools/WWW_Find/find_theorems.ML
     1.1 --- a/NEWS	Mon May 31 19:36:13 2010 +0200
     1.2 +++ b/NEWS	Mon May 31 21:06:57 2010 +0200
     1.3 @@ -503,9 +503,12 @@
     1.4    OuterLex      ~>  Token
     1.5    OuterParse    ~>  Parse
     1.6    OuterSyntax   ~>  Outer_Syntax
     1.7 +  PrintMode     ~>  Print_Mode
     1.8    SpecParse     ~>  Parse_Spec
     1.9 +  ThyInfo       ~>  Thy_Info
    1.10 +  ThyLoad       ~>  Thy_Load
    1.11 +  ThyOutput     ~>  Thy_Output
    1.12    TypeInfer     ~>  Type_Infer
    1.13 -  PrintMode     ~>  Print_Mode
    1.14  
    1.15  Note that "open Legacy" simplifies porting of sources, but forgetting
    1.16  to remove it again will complicate porting again in the future.
     2.1 --- a/doc-src/Classes/Thy/document/Classes.tex	Mon May 31 19:36:13 2010 +0200
     2.2 +++ b/doc-src/Classes/Thy/document/Classes.tex	Mon May 31 21:06:57 2010 +0200
     2.3 @@ -792,8 +792,7 @@
     2.4  \isamarkuptrue%
     2.5  %
     2.6  \begin{isamarkuptext}%
     2.7 -Isabelle locales support a concept of local definitions
     2.8 -  in locales:%
     2.9 +Isabelle locales are targets which support local definitions:%
    2.10  \end{isamarkuptext}%
    2.11  \isamarkuptrue%
    2.12  %
     3.1 --- a/doc-src/IsarImplementation/Thy/Integration.thy	Mon May 31 19:36:13 2010 +0200
     3.2 +++ b/doc-src/IsarImplementation/Thy/Integration.thy	Mon May 31 21:06:57 2010 +0200
     3.3 @@ -368,13 +368,13 @@
     3.4    @{index_ML theory: "string -> theory"} \\
     3.5    @{index_ML use_thy: "string -> unit"} \\
     3.6    @{index_ML use_thys: "string list -> unit"} \\
     3.7 -  @{index_ML ThyInfo.touch_thy: "string -> unit"} \\
     3.8 -  @{index_ML ThyInfo.remove_thy: "string -> unit"} \\[1ex]
     3.9 -  @{index_ML ThyInfo.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
    3.10 -  @{index_ML ThyInfo.end_theory: "theory -> unit"} \\
    3.11 -  @{index_ML ThyInfo.register_theory: "theory -> unit"} \\[1ex]
    3.12 +  @{index_ML Thy_Info.touch_thy: "string -> unit"} \\
    3.13 +  @{index_ML Thy_Info.remove_thy: "string -> unit"} \\[1ex]
    3.14 +  @{index_ML Thy_Info.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
    3.15 +  @{index_ML Thy_Info.end_theory: "theory -> unit"} \\
    3.16 +  @{index_ML Thy_Info.register_theory: "theory -> unit"} \\[1ex]
    3.17    @{verbatim "datatype action = Update | Outdate | Remove"} \\
    3.18 -  @{index_ML ThyInfo.add_hook: "(ThyInfo.action -> string -> unit) -> unit"} \\
    3.19 +  @{index_ML Thy_Info.add_hook: "(Thy_Info.action -> string -> unit) -> unit"} \\
    3.20    \end{mldecls}
    3.21  
    3.22    \begin{description}
    3.23 @@ -395,24 +395,24 @@
    3.24    intrinsic parallelism can be exploited by the system, to speedup
    3.25    loading.
    3.26  
    3.27 -  \item @{ML ThyInfo.touch_thy}~@{text A} performs and @{text outdate} action
    3.28 +  \item @{ML Thy_Info.touch_thy}~@{text A} performs and @{text outdate} action
    3.29    on theory @{text A} and all descendants.
    3.30  
    3.31 -  \item @{ML ThyInfo.remove_thy}~@{text A} deletes theory @{text A} and all
    3.32 +  \item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all
    3.33    descendants from the theory database.
    3.34  
    3.35 -  \item @{ML ThyInfo.begin_theory} is the basic operation behind a
    3.36 +  \item @{ML Thy_Info.begin_theory} is the basic operation behind a
    3.37    @{text \<THEORY>} header declaration.  This {\ML} function is
    3.38    normally not invoked directly.
    3.39  
    3.40 -  \item @{ML ThyInfo.end_theory} concludes the loading of a theory
    3.41 +  \item @{ML Thy_Info.end_theory} concludes the loading of a theory
    3.42    proper and stores the result in the theory database.
    3.43  
    3.44 -  \item @{ML ThyInfo.register_theory}~@{text "text thy"} registers an
    3.45 +  \item @{ML Thy_Info.register_theory}~@{text "text thy"} registers an
    3.46    existing theory value with the theory loader database.  There is no
    3.47    management of associated sources.
    3.48  
    3.49 -  \item @{ML "ThyInfo.add_hook"}~@{text f} registers function @{text
    3.50 +  \item @{ML "Thy_Info.add_hook"}~@{text f} registers function @{text
    3.51    f} as a hook for theory database actions.  The function will be
    3.52    invoked with the action and theory name being involved; thus derived
    3.53    actions may be performed in associated system components, e.g.\
     4.1 --- a/doc-src/IsarImplementation/Thy/document/Integration.tex	Mon May 31 19:36:13 2010 +0200
     4.2 +++ b/doc-src/IsarImplementation/Thy/document/Integration.tex	Mon May 31 21:06:57 2010 +0200
     4.3 @@ -440,13 +440,13 @@
     4.4    \indexdef{}{ML}{theory}\verb|theory: string -> theory| \\
     4.5    \indexdef{}{ML}{use\_thy}\verb|use_thy: string -> unit| \\
     4.6    \indexdef{}{ML}{use\_thys}\verb|use_thys: string list -> unit| \\
     4.7 -  \indexdef{}{ML}{ThyInfo.touch\_thy}\verb|ThyInfo.touch_thy: string -> unit| \\
     4.8 -  \indexdef{}{ML}{ThyInfo.remove\_thy}\verb|ThyInfo.remove_thy: string -> unit| \\[1ex]
     4.9 -  \indexdef{}{ML}{ThyInfo.begin\_theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
    4.10 -  \indexdef{}{ML}{ThyInfo.end\_theory}\verb|ThyInfo.end_theory: theory -> unit| \\
    4.11 -  \indexdef{}{ML}{ThyInfo.register\_theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
    4.12 +  \indexdef{}{ML}{Thy\_Info.touch\_thy}\verb|Thy_Info.touch_thy: string -> unit| \\
    4.13 +  \indexdef{}{ML}{Thy\_Info.remove\_thy}\verb|Thy_Info.remove_thy: string -> unit| \\[1ex]
    4.14 +  \indexdef{}{ML}{Thy\_Info.begin\_theory}\verb|Thy_Info.begin_theory|\verb|: ... -> bool -> theory| \\
    4.15 +  \indexdef{}{ML}{Thy\_Info.end\_theory}\verb|Thy_Info.end_theory: theory -> unit| \\
    4.16 +  \indexdef{}{ML}{Thy\_Info.register\_theory}\verb|Thy_Info.register_theory: theory -> unit| \\[1ex]
    4.17    \verb|datatype action = Update |\verb,|,\verb| Outdate |\verb,|,\verb| Remove| \\
    4.18 -  \indexdef{}{ML}{ThyInfo.add\_hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
    4.19 +  \indexdef{}{ML}{Thy\_Info.add\_hook}\verb|Thy_Info.add_hook: (Thy_Info.action -> string -> unit) -> unit| \\
    4.20    \end{mldecls}
    4.21  
    4.22    \begin{description}
    4.23 @@ -466,24 +466,24 @@
    4.24    intrinsic parallelism can be exploited by the system, to speedup
    4.25    loading.
    4.26  
    4.27 -  \item \verb|ThyInfo.touch_thy|~\isa{A} performs and \isa{outdate} action
    4.28 +  \item \verb|Thy_Info.touch_thy|~\isa{A} performs and \isa{outdate} action
    4.29    on theory \isa{A} and all descendants.
    4.30  
    4.31 -  \item \verb|ThyInfo.remove_thy|~\isa{A} deletes theory \isa{A} and all
    4.32 +  \item \verb|Thy_Info.remove_thy|~\isa{A} deletes theory \isa{A} and all
    4.33    descendants from the theory database.
    4.34  
    4.35 -  \item \verb|ThyInfo.begin_theory| is the basic operation behind a
    4.36 +  \item \verb|Thy_Info.begin_theory| is the basic operation behind a
    4.37    \isa{{\isasymTHEORY}} header declaration.  This {\ML} function is
    4.38    normally not invoked directly.
    4.39  
    4.40 -  \item \verb|ThyInfo.end_theory| concludes the loading of a theory
    4.41 +  \item \verb|Thy_Info.end_theory| concludes the loading of a theory
    4.42    proper and stores the result in the theory database.
    4.43  
    4.44 -  \item \verb|ThyInfo.register_theory|~\isa{text\ thy} registers an
    4.45 +  \item \verb|Thy_Info.register_theory|~\isa{text\ thy} registers an
    4.46    existing theory value with the theory loader database.  There is no
    4.47    management of associated sources.
    4.48  
    4.49 -  \item \verb|ThyInfo.add_hook|~\isa{f} registers function \isa{f} as a hook for theory database actions.  The function will be
    4.50 +  \item \verb|Thy_Info.add_hook|~\isa{f} registers function \isa{f} as a hook for theory database actions.  The function will be
    4.51    invoked with the action and theory name being involved; thus derived
    4.52    actions may be performed in associated system components, e.g.\
    4.53    maintaining the state of an editor for the theory sources.
     5.1 --- a/doc-src/IsarRef/Thy/ROOT-HOLCF.ML	Mon May 31 19:36:13 2010 +0200
     5.2 +++ b/doc-src/IsarRef/Thy/ROOT-HOLCF.ML	Mon May 31 21:06:57 2010 +0200
     5.3 @@ -1,4 +1,4 @@
     5.4 -Unsynchronized.set ThyOutput.source;
     5.5 +Unsynchronized.set Thy_Output.source;
     5.6  use "../../antiquote_setup.ML";
     5.7  
     5.8  use_thy "HOLCF_Specific";
     6.1 --- a/doc-src/IsarRef/Thy/ROOT-ZF.ML	Mon May 31 19:36:13 2010 +0200
     6.2 +++ b/doc-src/IsarRef/Thy/ROOT-ZF.ML	Mon May 31 21:06:57 2010 +0200
     6.3 @@ -1,4 +1,4 @@
     6.4 -Unsynchronized.set ThyOutput.source;
     6.5 +Unsynchronized.set Thy_Output.source;
     6.6  use "../../antiquote_setup.ML";
     6.7  
     6.8  use_thy "ZF_Specific";
     7.1 --- a/doc-src/IsarRef/Thy/ROOT.ML	Mon May 31 19:36:13 2010 +0200
     7.2 +++ b/doc-src/IsarRef/Thy/ROOT.ML	Mon May 31 21:06:57 2010 +0200
     7.3 @@ -1,5 +1,5 @@
     7.4  Unsynchronized.set quick_and_dirty;
     7.5 -Unsynchronized.set ThyOutput.source;
     7.6 +Unsynchronized.set Thy_Output.source;
     7.7  use "../../antiquote_setup.ML";
     7.8  
     7.9  use_thys [
     8.1 --- a/doc-src/Main/Docs/Main_Doc.thy	Mon May 31 19:36:13 2010 +0200
     8.2 +++ b/doc-src/Main/Docs/Main_Doc.thy	Mon May 31 21:06:57 2010 +0200
     8.3 @@ -9,10 +9,10 @@
     8.4     else error "term_type_only: type mismatch";
     8.5     Syntax.pretty_typ ctxt T)
     8.6  
     8.7 -val _ = ThyOutput.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev)
     8.8 +val _ = Thy_Output.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev)
     8.9    (fn {source, context, ...} => fn arg =>
    8.10 -    ThyOutput.output
    8.11 -      (ThyOutput.maybe_pretty_source (pretty_term_type_only context) source [arg]));
    8.12 +    Thy_Output.output
    8.13 +      (Thy_Output.maybe_pretty_source (pretty_term_type_only context) source [arg]));
    8.14  *}
    8.15  (*>*)
    8.16  text{*
     9.1 --- a/doc-src/System/Thy/ROOT.ML	Mon May 31 19:36:13 2010 +0200
     9.2 +++ b/doc-src/System/Thy/ROOT.ML	Mon May 31 21:06:57 2010 +0200
     9.3 @@ -1,4 +1,4 @@
     9.4 -Unsynchronized.set ThyOutput.source;
     9.5 +Unsynchronized.set Thy_Output.source;
     9.6  use "../../antiquote_setup.ML";
     9.7  
     9.8  use_thys ["Basics", "Interfaces", "Presentation", "Misc"];
    10.1 --- a/doc-src/TutorialI/Rules/Primes.thy	Mon May 31 19:36:13 2010 +0200
    10.2 +++ b/doc-src/TutorialI/Rules/Primes.thy	Mon May 31 21:06:57 2010 +0200
    10.3 @@ -10,7 +10,7 @@
    10.4  
    10.5  
    10.6  ML "Pretty.margin_default := 64"
    10.7 -ML "ThyOutput.indent := 5"  (*that is, Doc/TutorialI/settings.ML*)
    10.8 +ML "Thy_Output.indent := 5"  (*that is, Doc/TutorialI/settings.ML*)
    10.9  
   10.10  
   10.11  text {*Now in Basic.thy!
    11.1 --- a/doc-src/TutorialI/Types/Numbers.thy	Mon May 31 19:36:13 2010 +0200
    11.2 +++ b/doc-src/TutorialI/Types/Numbers.thy	Mon May 31 21:06:57 2010 +0200
    11.3 @@ -3,7 +3,7 @@
    11.4  begin
    11.5  
    11.6  ML "Pretty.margin_default := 64"
    11.7 -ML "ThyOutput.indent := 0"  (*we don't want 5 for listing theorems*)
    11.8 +ML "Thy_Output.indent := 0"  (*we don't want 5 for listing theorems*)
    11.9  
   11.10  text{*
   11.11  
    12.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex	Mon May 31 19:36:13 2010 +0200
    12.2 +++ b/doc-src/TutorialI/Types/document/Numbers.tex	Mon May 31 21:06:57 2010 +0200
    12.3 @@ -28,7 +28,7 @@
    12.4  \isacommand{ML}\isamarkupfalse%
    12.5  \ {\isachardoublequoteopen}Pretty{\isachardot}margin{\isacharunderscore}default\ {\isacharcolon}{\isacharequal}\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}\isanewline
    12.6  \isacommand{ML}\isamarkupfalse%
    12.7 -\ {\isachardoublequoteopen}ThyOutput{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
    12.8 +\ {\isachardoublequoteopen}Thy{\isacharunderscore}Output{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
    12.9  \endisatagML
   12.10  {\isafoldML}%
   12.11  %
    13.1 --- a/doc-src/TutorialI/Types/document/Pairs.tex	Mon May 31 19:36:13 2010 +0200
    13.2 +++ b/doc-src/TutorialI/Types/document/Pairs.tex	Mon May 31 21:06:57 2010 +0200
    13.3 @@ -60,7 +60,7 @@
    13.4  Internally, \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ t} becomes \isa{split\ {\isacharparenleft}{\isasymlambda}x\ y{\isachardot}\ t{\isacharparenright}}, where
    13.5  \cdx{split} is the uncurrying function of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c} defined as
    13.6  \begin{center}
    13.7 -\isa{split\ {\isasymequiv}\ {\isasymlambda}c\ p{\isachardot}\ c\ {\isacharparenleft}fst\ p{\isacharparenright}\ {\isacharparenleft}snd\ p{\isacharparenright}}
    13.8 +\isa{split\ {\isacharequal}\ {\isacharparenleft}{\isasymlambda}c\ p{\isachardot}\ c\ {\isacharparenleft}fst\ p{\isacharparenright}\ {\isacharparenleft}snd\ p{\isacharparenright}{\isacharparenright}}
    13.9  \hfill(\isa{split{\isacharunderscore}def})
   13.10  \end{center}
   13.11  Pattern matching in
    14.1 --- a/doc-src/TutorialI/settings.ML	Mon May 31 19:36:13 2010 +0200
    14.2 +++ b/doc-src/TutorialI/settings.ML	Mon May 31 21:06:57 2010 +0200
    14.3 @@ -1,3 +1,3 @@
    14.4  (* $Id$ *)
    14.5  
    14.6 -ThyOutput.indent := 5;
    14.7 +Thy_Output.indent := 5;
    15.1 --- a/doc-src/antiquote_setup.ML	Mon May 31 19:36:13 2010 +0200
    15.2 +++ b/doc-src/antiquote_setup.ML	Mon May 31 21:06:57 2010 +0200
    15.3 @@ -35,7 +35,7 @@
    15.4  
    15.5  val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|";
    15.6  
    15.7 -val _ = ThyOutput.antiquotation "verbatim" (Scan.lift Args.name)
    15.8 +val _ = Thy_Output.antiquotation "verbatim" (Scan.lift Args.name)
    15.9    (K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"));
   15.10  
   15.11  
   15.12 @@ -56,7 +56,7 @@
   15.13  
   15.14  fun ml_functor (txt, _) = "ML_Env.check_functor " ^ ML_Syntax.print_string txt;
   15.15  
   15.16 -fun index_ml name kind ml = ThyOutput.antiquotation name
   15.17 +fun index_ml name kind ml = Thy_Output.antiquotation name
   15.18    (Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) ""))
   15.19    (fn {context = ctxt, ...} => fn (txt1, txt2) =>
   15.20      let
   15.21 @@ -71,8 +71,8 @@
   15.22      in
   15.23        "\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string txt1 ^ "}" ^
   15.24        (txt'
   15.25 -      |> (if ! ThyOutput.quotes then quote else I)
   15.26 -      |> (if ! ThyOutput.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
   15.27 +      |> (if ! Thy_Output.quotes then quote else I)
   15.28 +      |> (if ! Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
   15.29            else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
   15.30      end);
   15.31  
   15.32 @@ -89,30 +89,30 @@
   15.33  
   15.34  (* named theorems *)
   15.35  
   15.36 -val _ = ThyOutput.antiquotation "named_thms"
   15.37 +val _ = Thy_Output.antiquotation "named_thms"
   15.38    (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
   15.39    (fn {context = ctxt, ...} =>
   15.40 -    map (apfst (ThyOutput.pretty_thm ctxt))
   15.41 -    #> (if ! ThyOutput.quotes then map (apfst Pretty.quote) else I)
   15.42 -    #> (if ! ThyOutput.display
   15.43 +    map (apfst (Thy_Output.pretty_thm ctxt))
   15.44 +    #> (if ! Thy_Output.quotes then map (apfst Pretty.quote) else I)
   15.45 +    #> (if ! Thy_Output.display
   15.46          then
   15.47            map (fn (p, name) =>
   15.48 -            Output.output (Pretty.string_of (Pretty.indent (! ThyOutput.indent) p)) ^
   15.49 -            "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
   15.50 +            Output.output (Pretty.string_of (Pretty.indent (! Thy_Output.indent) p)) ^
   15.51 +            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}")
   15.52            #> space_implode "\\par\\smallskip%\n"
   15.53            #> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   15.54          else
   15.55            map (fn (p, name) =>
   15.56              Output.output (Pretty.str_of p) ^
   15.57 -            "\\rulename{" ^ Output.output (Pretty.str_of (ThyOutput.pretty_text name)) ^ "}")
   15.58 +            "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text name)) ^ "}")
   15.59            #> space_implode "\\par\\smallskip%\n"
   15.60            #> enclose "\\isa{" "}"));
   15.61  
   15.62  
   15.63  (* theory file *)
   15.64  
   15.65 -val _ = ThyOutput.antiquotation "thy_file" (Scan.lift Args.name)
   15.66 -  (fn _ => fn name => (ThyLoad.check_thy Path.current name; ThyOutput.output [Pretty.str name]));
   15.67 +val _ = Thy_Output.antiquotation "thy_file" (Scan.lift Args.name)
   15.68 +  (fn _ => fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output [Pretty.str name]));
   15.69  
   15.70  
   15.71  (* Isabelle/Isar entities (with index) *)
   15.72 @@ -131,7 +131,7 @@
   15.73  val arg = enclose "{" "}" o clean_string;
   15.74  
   15.75  fun entity check markup kind index =
   15.76 -  ThyOutput.antiquotation
   15.77 +  Thy_Output.antiquotation
   15.78      (translate (fn " " => "_" | c => c) kind ^
   15.79        (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))
   15.80      (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
   15.81 @@ -152,8 +152,8 @@
   15.82            idx ^
   15.83            (Output.output name
   15.84              |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
   15.85 -            |> (if ! ThyOutput.quotes then quote else I)
   15.86 -            |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   15.87 +            |> (if ! Thy_Output.quotes then quote else I)
   15.88 +            |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   15.89                  else hyper o enclose "\\mbox{\\isa{" "}}"))
   15.90          else error ("Bad " ^ kind ^ " " ^ quote name)
   15.91        end);
   15.92 @@ -174,14 +174,14 @@
   15.93  val _ = entity_antiqs no_check "" "fact";
   15.94  val _ = entity_antiqs no_check "" "variable";
   15.95  val _ = entity_antiqs no_check "" "case";
   15.96 -val _ = entity_antiqs (K ThyOutput.defined_command) "" "antiquotation";
   15.97 -val _ = entity_antiqs (K ThyOutput.defined_option) "" "antiquotation option";
   15.98 +val _ = entity_antiqs (K Thy_Output.defined_command) "" "antiquotation";
   15.99 +val _ = entity_antiqs (K Thy_Output.defined_option) "" "antiquotation option";
  15.100  val _ = entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting";
  15.101  val _ = entity_antiqs no_check "" "inference";
  15.102  val _ = entity_antiqs no_check "isatt" "executable";
  15.103  val _ = entity_antiqs (K check_tool) "isatt" "tool";
  15.104  val _ = entity_antiqs (K (File.exists o Path.explode)) "isatt" "file";
  15.105 -val _ = entity_antiqs (K ThyInfo.known_thy) "" "theory";
  15.106 +val _ = entity_antiqs (K Thy_Info.known_thy) "" "theory";
  15.107  
  15.108  end;
  15.109  
    16.1 --- a/doc-src/more_antiquote.ML	Mon May 31 19:36:13 2010 +0200
    16.2 +++ b/doc-src/more_antiquote.ML	Mon May 31 21:06:57 2010 +0200
    16.3 @@ -64,8 +64,8 @@
    16.4  
    16.5  in
    16.6  
    16.7 -val _ = ThyOutput.antiquotation "class" (Scan.lift Args.name) (pr_class o #context);
    16.8 -val _ = ThyOutput.antiquotation "type" (Scan.lift Args.name) (pr_type o #context);
    16.9 +val _ = Thy_Output.antiquotation "class" (Scan.lift Args.name) (pr_class o #context);
   16.10 +val _ = Thy_Output.antiquotation "type" (Scan.lift Args.name) (pr_type o #context);
   16.11  
   16.12  end;
   16.13  
   16.14 @@ -95,11 +95,11 @@
   16.15        |> snd
   16.16        |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
   16.17        |> map (holize o no_vars ctxt o AxClass.overload thy);
   16.18 -  in ThyOutput.output (ThyOutput.maybe_pretty_source (pretty_thm ctxt) src thms) end;
   16.19 +  in Thy_Output.output (Thy_Output.maybe_pretty_source (pretty_thm ctxt) src thms) end;
   16.20  
   16.21  in
   16.22  
   16.23 -val _ = ThyOutput.antiquotation "code_thms" Args.term
   16.24 +val _ = Thy_Output.antiquotation "code_thms" Args.term
   16.25    (fn {source, context, ...} => pretty_code_thm source context);
   16.26  
   16.27  end;
   16.28 @@ -123,7 +123,7 @@
   16.29  
   16.30  in
   16.31  
   16.32 -val _ = ThyOutput.antiquotation "code_stmts"
   16.33 +val _ = Thy_Output.antiquotation "code_stmts"
   16.34    (parse_const_terms -- Scan.repeat parse_names -- Scan.lift (Args.parens Args.name))
   16.35    (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), target) =>
   16.36      let val thy = ProofContext.theory_of ctxt in
    17.1 --- a/doc-src/rail.ML	Mon May 31 19:36:13 2010 +0200
    17.2 +++ b/doc-src/rail.ML	Mon May 31 21:06:57 2010 +0200
    17.3 @@ -67,14 +67,14 @@
    17.4    ("fact", ("", no_check, true)),
    17.5    ("variable", ("", no_check, true)),
    17.6    ("case", ("", no_check, true)),
    17.7 -  ("antiquotation", ("", K ThyOutput.defined_command, true)),
    17.8 -  ("antiquotation option", ("", K ThyOutput.defined_option, true)), (* kann mein scanner nicht erkennen *)
    17.9 +  ("antiquotation", ("", K Thy_Output.defined_command, true)),
   17.10 +  ("antiquotation option", ("", K Thy_Output.defined_option, true)), (* kann mein scanner nicht erkennen *)
   17.11    ("setting", ("isatt", (fn _ => fn name => is_some (OS.Process.getEnv name)), true)),
   17.12    ("inference", ("", no_check, true)),
   17.13    ("executable", ("isatt", no_check, true)),
   17.14    ("tool", ("isatt", K check_tool, true)),
   17.15    ("file", ("isatt", K (File.exists o Path.explode), true)),
   17.16 -  ("theory", ("", K ThyInfo.known_thy, true))
   17.17 +  ("theory", ("", K Thy_Info.known_thy, true))
   17.18    ];
   17.19  
   17.20  in
   17.21 @@ -97,8 +97,8 @@
   17.22      (idx ^
   17.23      (Output.output name
   17.24        |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
   17.25 -      |> (if ! ThyOutput.quotes then quote else I)
   17.26 -      |> (if ! ThyOutput.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   17.27 +      |> (if ! Thy_Output.quotes then quote else I)
   17.28 +      |> (if ! Thy_Output.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
   17.29            else hyper o enclose "\\mbox{\\isa{" "}}")), style)
   17.30    else ("Bad " ^ kind ^ " " ^ name, false)
   17.31    end;
   17.32 @@ -473,7 +473,7 @@
   17.33    |> parse
   17.34    |> print;
   17.35  
   17.36 -val _ = ThyOutput.antiquotation "rail" (Scan.lift (Parse.position Args.name))
   17.37 +val _ = Thy_Output.antiquotation "rail" (Scan.lift (Parse.position Args.name))
   17.38    (fn {context = ctxt,...} => fn txt => process txt ctxt);
   17.39  
   17.40  end;
    18.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon May 31 19:36:13 2010 +0200
    18.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon May 31 21:06:57 2010 +0200
    18.3 @@ -219,7 +219,7 @@
    18.4              then NONE
    18.5              else
    18.6                let
    18.7 -                val _ = List.app (SimpleThread.interrupt o #1) cancelling;
    18.8 +                val _ = List.app (Simple_Thread.interrupt o #1) cancelling;
    18.9                  val cancelling' = filter (Thread.isActive o #1) cancelling;
   18.10                  val state' = make_state manager timeout_heap' active cancelling' messages store;
   18.11                in SOME (map #2 timeout_threads, state') end
    19.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Mon May 31 19:36:13 2010 +0200
    19.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Mon May 31 21:06:57 2010 +0200
    19.3 @@ -236,7 +236,7 @@
    19.4  
    19.5  (** document antiquotation **)
    19.6  
    19.7 -val _ = ThyOutput.antiquotation "datatype" (Args.type_name true)
    19.8 +val _ = Thy_Output.antiquotation "datatype" (Args.type_name true)
    19.9    (fn {source = src, context = ctxt, ...} => fn dtco =>
   19.10      let
   19.11        val thy = ProofContext.theory_of ctxt;
   19.12 @@ -257,7 +257,7 @@
   19.13             Pretty.str " =" :: Pretty.brk 1 ::
   19.14             flat (separate [Pretty.brk 1, Pretty.str "| "]
   19.15               (map (single o pretty_constr) cos)));
   19.16 -    in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end);
   19.17 +    in Thy_Output.output (Thy_Output.maybe_pretty_source (K pretty_datatype) src [()]) end);
   19.18  
   19.19  
   19.20  
    20.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon May 31 19:36:13 2010 +0200
    20.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon May 31 21:06:57 2010 +0200
    20.3 @@ -181,7 +181,7 @@
    20.4      val ctxt = Proof.context_of state
    20.5  (* FIXME: reintroduce code before new release:
    20.6  
    20.7 -    val nitpick_thy = ThyInfo.get_theory "Nitpick"
    20.8 +    val nitpick_thy = Thy_Info.get_theory "Nitpick"
    20.9      val _ = Theory.subthy (nitpick_thy, thy) orelse
   20.10              error "You must import the theory \"Nitpick\" to use Nitpick"
   20.11  *)
    21.1 --- a/src/Pure/Concurrent/future.ML	Mon May 31 19:36:13 2010 +0200
    21.2 +++ b/src/Pure/Concurrent/future.ML	Mon May 31 21:06:57 2010 +0200
    21.3 @@ -126,7 +126,7 @@
    21.4    val lock = Mutex.mutex ();
    21.5  in
    21.6  
    21.7 -fun SYNCHRONIZED name = SimpleThread.synchronized name lock;
    21.8 +fun SYNCHRONIZED name = Simple_Thread.synchronized name lock;
    21.9  
   21.10  fun wait cond = (*requires SYNCHRONIZED*)
   21.11    Multithreading.sync_wait NONE NONE cond lock;
   21.12 @@ -238,7 +238,7 @@
   21.13    | SOME work => (execute work; worker_loop name));
   21.14  
   21.15  fun worker_start name = (*requires SYNCHRONIZED*)
   21.16 -  Unsynchronized.change workers (cons (SimpleThread.fork false (fn () => worker_loop name),
   21.17 +  Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
   21.18      Unsynchronized.ref Working));
   21.19  
   21.20  
   21.21 @@ -371,7 +371,7 @@
   21.22  fun scheduler_check () = (*requires SYNCHRONIZED*)
   21.23   (do_shutdown := false;
   21.24    if scheduler_active () then ()
   21.25 -  else scheduler := SOME (SimpleThread.fork false scheduler_loop));
   21.26 +  else scheduler := SOME (Simple_Thread.fork false scheduler_loop));
   21.27  
   21.28  
   21.29  
    22.1 --- a/src/Pure/Concurrent/simple_thread.ML	Mon May 31 19:36:13 2010 +0200
    22.2 +++ b/src/Pure/Concurrent/simple_thread.ML	Mon May 31 21:06:57 2010 +0200
    22.3 @@ -12,7 +12,7 @@
    22.4    val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
    22.5  end;
    22.6  
    22.7 -structure SimpleThread: SIMPLE_THREAD =
    22.8 +structure Simple_Thread: SIMPLE_THREAD =
    22.9  struct
   22.10  
   22.11  fun attributes interrupts =
    23.1 --- a/src/Pure/Concurrent/single_assignment.ML	Mon May 31 19:36:13 2010 +0200
    23.2 +++ b/src/Pure/Concurrent/single_assignment.ML	Mon May 31 21:06:57 2010 +0200
    23.3 @@ -32,7 +32,7 @@
    23.4  fun peek (Var {var, ...}) = SingleAssignment.savalue var;
    23.5  
    23.6  fun await (v as Var {name, lock, cond, var}) =
    23.7 -  SimpleThread.synchronized name lock (fn () =>
    23.8 +  Simple_Thread.synchronized name lock (fn () =>
    23.9      let
   23.10        fun wait () =
   23.11          (case peek v of
   23.12 @@ -44,7 +44,7 @@
   23.13      in wait () end);
   23.14  
   23.15  fun assign (v as Var {name, lock, cond, var}) x =
   23.16 -  SimpleThread.synchronized name lock (fn () =>
   23.17 +  Simple_Thread.synchronized name lock (fn () =>
   23.18      (case peek v of
   23.19        SOME _ => raise Fail ("Duplicate assignment to variable " ^ quote name)
   23.20      | NONE =>
    24.1 --- a/src/Pure/Concurrent/synchronized.ML	Mon May 31 19:36:13 2010 +0200
    24.2 +++ b/src/Pure/Concurrent/synchronized.ML	Mon May 31 21:06:57 2010 +0200
    24.3 @@ -39,7 +39,7 @@
    24.4  (* synchronized access *)
    24.5  
    24.6  fun timed_access (Var {name, lock, cond, var}) time_limit f =
    24.7 -  SimpleThread.synchronized name lock (fn () =>
    24.8 +  Simple_Thread.synchronized name lock (fn () =>
    24.9      let
   24.10        fun try_change () =
   24.11          let val x = ! var in
    25.1 --- a/src/Pure/Concurrent/task_queue.ML	Mon May 31 19:36:13 2010 +0200
    25.2 +++ b/src/Pure/Concurrent/task_queue.ML	Mon May 31 21:06:57 2010 +0200
    25.3 @@ -162,7 +162,7 @@
    25.4      val tasks = Inttab.lookup_list groups (group_id group);
    25.5      val running =
    25.6        fold (get_job jobs #> (fn Running t => insert Thread.equal t | _ => I)) tasks [];
    25.7 -    val _ = List.app SimpleThread.interrupt running;
    25.8 +    val _ = List.app Simple_Thread.interrupt running;
    25.9    in null running end;
   25.10  
   25.11  fun cancel_all (Queue {groups, jobs}) =
   25.12 @@ -173,7 +173,7 @@
   25.13            Running t => (insert eq_group group groups, insert Thread.equal t running)
   25.14          | _ => (groups, running)));
   25.15      val (running_groups, running) = Task_Graph.fold (cancel_job o #1 o #2) jobs ([], []);
   25.16 -    val _ = List.app SimpleThread.interrupt running;
   25.17 +    val _ = List.app Simple_Thread.interrupt running;
   25.18    in running_groups end;
   25.19  
   25.20  
    26.1 --- a/src/Pure/General/scan.ML	Mon May 31 19:36:13 2010 +0200
    26.2 +++ b/src/Pure/General/scan.ML	Mon May 31 21:06:57 2010 +0200
    26.3 @@ -322,5 +322,5 @@
    26.4  
    26.5  end;
    26.6  
    26.7 -structure BasicScan: BASIC_SCAN = Scan;
    26.8 -open BasicScan;
    26.9 +structure Basic_Scan: BASIC_SCAN = Scan;
   26.10 +open Basic_Scan;
    27.1 --- a/src/Pure/Isar/isar_cmd.ML	Mon May 31 19:36:13 2010 +0200
    27.2 +++ b/src/Pure/Isar/isar_cmd.ML	Mon May 31 21:06:57 2010 +0200
    27.3 @@ -85,7 +85,7 @@
    27.4    val proof_markup: Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
    27.5  end;
    27.6  
    27.7 -structure IsarCmd: ISAR_CMD =
    27.8 +structure Isar_Cmd: ISAR_CMD =
    27.9  struct
   27.10  
   27.11  
   27.12 @@ -272,10 +272,10 @@
   27.13  (* init and exit *)
   27.14  
   27.15  fun init_theory (name, imports, uses) =
   27.16 -  Toplevel.init_theory name (ThyInfo.begin_theory name imports (map (apfst Path.explode) uses))
   27.17 +  Toplevel.init_theory name (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses))
   27.18      (fn thy =>
   27.19 -      if ThyInfo.check_known_thy (Context.theory_name thy)
   27.20 -      then ThyInfo.end_theory thy else ());
   27.21 +      if Thy_Info.check_known_thy (Context.theory_name thy)
   27.22 +      then Thy_Info.end_theory thy else ());
   27.23  
   27.24  val exit = Toplevel.keep (fn state =>
   27.25   (Context.set_thread_data (try Toplevel.generic_theory_of state);
   27.26 @@ -384,18 +384,18 @@
   27.27  val print_methods = Toplevel.unknown_theory o
   27.28    Toplevel.keep (Method.print_methods o Toplevel.theory_of);
   27.29  
   27.30 -val print_antiquotations = Toplevel.imperative ThyOutput.print_antiquotations;
   27.31 +val print_antiquotations = Toplevel.imperative Thy_Output.print_antiquotations;
   27.32  
   27.33  val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   27.34    let
   27.35      val thy = Toplevel.theory_of state;
   27.36 -    val all_thys = sort ThyInfo.thy_ord (thy :: Theory.ancestors_of thy);
   27.37 +    val all_thys = sort Thy_Info.thy_ord (thy :: Theory.ancestors_of thy);
   27.38      val gr = all_thys |> map (fn node =>
   27.39        let
   27.40          val name = Context.theory_name node;
   27.41          val parents = map Context.theory_name (Theory.parents_of node);
   27.42          val dir = Present.session_name node;
   27.43 -        val unfold = not (ThyInfo.known_thy name andalso ThyInfo.is_finished name);
   27.44 +        val unfold = not (Thy_Info.known_thy name andalso Thy_Info.is_finished name);
   27.45        in {name = name, ID = name, parents = parents, dir = dir, unfold = unfold, path = ""} end);
   27.46    in Present.display_graph gr end);
   27.47  
   27.48 @@ -427,8 +427,8 @@
   27.49      Thm_Deps.unused_thms
   27.50        (case opt_range of
   27.51          NONE => (Theory.parents_of thy, [thy])
   27.52 -      | SOME (xs, NONE) => (map ThyInfo.get_theory xs, [thy])
   27.53 -      | SOME (xs, SOME ys) => (map ThyInfo.get_theory xs, map ThyInfo.get_theory ys))
   27.54 +      | SOME (xs, NONE) => (map Thy_Info.get_theory xs, [thy])
   27.55 +      | SOME (xs, SOME ys) => (map Thy_Info.get_theory xs, map Thy_Info.get_theory ys))
   27.56      |> map pretty_thm |> Pretty.chunks |> Pretty.writeln
   27.57    end);
   27.58  
   27.59 @@ -517,7 +517,7 @@
   27.60  
   27.61  fun check_text (txt, pos) state =
   27.62   (Position.report Markup.doc_source pos;
   27.63 -  ignore (ThyOutput.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
   27.64 +  ignore (Thy_Output.eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
   27.65  
   27.66  fun header_markup txt = Toplevel.keep (fn state =>
   27.67    if Toplevel.is_toplevel state then check_text txt state
    28.1 --- a/src/Pure/Isar/isar_document.ML	Mon May 31 19:36:13 2010 +0200
    28.2 +++ b/src/Pure/Isar/isar_document.ML	Mon May 31 21:06:57 2010 +0200
    28.3 @@ -181,7 +181,7 @@
    28.4  
    28.5  fun begin_document (id: document_id) path =
    28.6    let
    28.7 -    val (dir, name) = ThyLoad.split_thy_path path;
    28.8 +    val (dir, name) = Thy_Load.split_thy_path path;
    28.9      val _ = define_document id (make_document dir name no_entries);
   28.10    in () end;
   28.11  
   28.12 @@ -197,8 +197,8 @@
   28.13            (case Lazy.force end_state of
   28.14              SOME st =>
   28.15               (Toplevel.run_command name (Toplevel.put_id id (Toplevel.commit_exit Position.none)) st;
   28.16 -              ThyInfo.touch_child_thys name;
   28.17 -              ThyInfo.register_thy name)
   28.18 +              Thy_Info.touch_child_thys name;
   28.19 +              Thy_Info.register_thy name)
   28.20            | NONE => error ("Failed to finish theory " ^ quote name)));
   28.21      in () end);
   28.22  
    29.1 --- a/src/Pure/Isar/isar_syn.ML	Mon May 31 19:36:13 2010 +0200
    29.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon May 31 21:06:57 2010 +0200
    29.3 @@ -4,7 +4,7 @@
    29.4  Isar/Pure outer syntax.
    29.5  *)
    29.6  
    29.7 -structure IsarSyn: sig end =
    29.8 +structure Isar_Syn: sig end =
    29.9  struct
   29.10  
   29.11  (** keywords **)
   29.12 @@ -28,7 +28,7 @@
   29.13  
   29.14  val _ =
   29.15    Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
   29.16 -    (Thy_Header.args >> (Toplevel.print oo IsarCmd.init_theory));
   29.17 +    (Thy_Header.args >> (Toplevel.print oo Isar_Cmd.init_theory));
   29.18  
   29.19  val _ =
   29.20    Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
   29.21 @@ -38,43 +38,43 @@
   29.22  
   29.23  (** markup commands **)
   29.24  
   29.25 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "header" "theory header" Keyword.diag
   29.26 -  (Parse.doc_source >> IsarCmd.header_markup);
   29.27 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "header" "theory header" Keyword.diag
   29.28 +  (Parse.doc_source >> Isar_Cmd.header_markup);
   29.29  
   29.30 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "chapter" "chapter heading"
   29.31 -  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
   29.32 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "chapter" "chapter heading"
   29.33 +  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
   29.34  
   29.35 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "section" "section heading"
   29.36 -  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
   29.37 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "section" "section heading"
   29.38 +  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
   29.39  
   29.40 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "subsection" "subsection heading"
   29.41 -  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
   29.42 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsection" "subsection heading"
   29.43 +  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
   29.44  
   29.45  val _ =
   29.46 -  Outer_Syntax.markup_command ThyOutput.Markup "subsubsection" "subsubsection heading"
   29.47 -  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
   29.48 +  Outer_Syntax.markup_command Thy_Output.Markup "subsubsection" "subsubsection heading"
   29.49 +  Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
   29.50  
   29.51 -val _ = Outer_Syntax.markup_command ThyOutput.MarkupEnv "text" "formal comment (theory)"
   29.52 -  Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
   29.53 +val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv "text" "formal comment (theory)"
   29.54 +  Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
   29.55  
   29.56 -val _ = Outer_Syntax.markup_command ThyOutput.Verbatim "text_raw" "raw document preparation text"
   29.57 -  Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> IsarCmd.local_theory_markup);
   29.58 +val _ = Outer_Syntax.markup_command Thy_Output.Verbatim "text_raw" "raw document preparation text"
   29.59 +  Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
   29.60  
   29.61 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "sect" "formal comment (proof)"
   29.62 -  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
   29.63 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "sect" "formal comment (proof)"
   29.64 +  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
   29.65  
   29.66 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "subsect" "formal comment (proof)"
   29.67 -  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
   29.68 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsect" "formal comment (proof)"
   29.69 +  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
   29.70  
   29.71 -val _ = Outer_Syntax.markup_command ThyOutput.Markup "subsubsect" "formal comment (proof)"
   29.72 -  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> IsarCmd.proof_markup);
   29.73 +val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsubsect" "formal comment (proof)"
   29.74 +  (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
   29.75  
   29.76 -val _ = Outer_Syntax.markup_command ThyOutput.MarkupEnv "txt" "formal comment (proof)"
   29.77 -  (Keyword.tag_proof Keyword.prf_decl) (Parse.doc_source >> IsarCmd.proof_markup);
   29.78 +val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv "txt" "formal comment (proof)"
   29.79 +  (Keyword.tag_proof Keyword.prf_decl) (Parse.doc_source >> Isar_Cmd.proof_markup);
   29.80  
   29.81 -val _ = Outer_Syntax.markup_command ThyOutput.Verbatim "txt_raw"
   29.82 +val _ = Outer_Syntax.markup_command Thy_Output.Verbatim "txt_raw"
   29.83    "raw document preparation text (proof)" (Keyword.tag_proof Keyword.prf_decl)
   29.84 -  (Parse.doc_source >> IsarCmd.proof_markup);
   29.85 +  (Parse.doc_source >> Isar_Cmd.proof_markup);
   29.86  
   29.87  
   29.88  
   29.89 @@ -185,7 +185,7 @@
   29.90    Outer_Syntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl
   29.91      (Scan.repeat1 Parse_Spec.spec >>
   29.92        (Toplevel.theory o
   29.93 -        (IsarCmd.add_axioms o
   29.94 +        (Isar_Cmd.add_axioms o
   29.95            tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead"))));
   29.96  
   29.97  val opt_unchecked_overloaded =
   29.98 @@ -197,7 +197,7 @@
   29.99    Outer_Syntax.command "defs" "define constants" Keyword.thy_decl
  29.100      (opt_unchecked_overloaded --
  29.101        Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
  29.102 -      >> (Toplevel.theory o IsarCmd.add_defs));
  29.103 +      >> (Toplevel.theory o Isar_Cmd.add_defs));
  29.104  
  29.105  
  29.106  (* old constdefs *)
  29.107 @@ -296,10 +296,10 @@
  29.108      ((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>
  29.109        (Toplevel.theory o uncurry hide));
  29.110  
  29.111 -val _ = hide_names "hide_class" IsarCmd.hide_class "classes";
  29.112 -val _ = hide_names "hide_type" IsarCmd.hide_type "types";
  29.113 -val _ = hide_names "hide_const" IsarCmd.hide_const "constants";
  29.114 -val _ = hide_names "hide_fact" IsarCmd.hide_fact "facts";
  29.115 +val _ = hide_names "hide_class" Isar_Cmd.hide_class "classes";
  29.116 +val _ = hide_names "hide_type" Isar_Cmd.hide_type "types";
  29.117 +val _ = hide_names "hide_const" Isar_Cmd.hide_const "constants";
  29.118 +val _ = hide_names "hide_fact" Isar_Cmd.hide_fact "facts";
  29.119  
  29.120  
  29.121  (* use ML text *)
  29.122 @@ -314,7 +314,7 @@
  29.123  val _ =
  29.124    Outer_Syntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
  29.125      (Parse.path >>
  29.126 -      (fn path => Toplevel.generic_theory (ThyInfo.exec_file false path #> propagate_env)));
  29.127 +      (fn path => Toplevel.generic_theory (Thy_Info.exec_file false path #> propagate_env)));
  29.128  
  29.129  val _ =
  29.130    Outer_Syntax.command "ML" "ML text within theory or local theory"
  29.131 @@ -331,19 +331,19 @@
  29.132  
  29.133  val _ =
  29.134    Outer_Syntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)
  29.135 -    (Parse.ML_source >> IsarCmd.ml_diag true);
  29.136 +    (Parse.ML_source >> Isar_Cmd.ml_diag true);
  29.137  
  29.138  val _ =
  29.139    Outer_Syntax.command "ML_command" "diagnostic ML text (silent)" (Keyword.tag_ml Keyword.diag)
  29.140 -    (Parse.ML_source >> (Toplevel.no_timing oo IsarCmd.ml_diag false));
  29.141 +    (Parse.ML_source >> (Toplevel.no_timing oo Isar_Cmd.ml_diag false));
  29.142  
  29.143  val _ =
  29.144    Outer_Syntax.command "setup" "ML theory setup" (Keyword.tag_ml Keyword.thy_decl)
  29.145 -    (Parse.ML_source >> (Toplevel.theory o IsarCmd.global_setup));
  29.146 +    (Parse.ML_source >> (Toplevel.theory o Isar_Cmd.global_setup));
  29.147  
  29.148  val _ =
  29.149    Outer_Syntax.local_theory "local_setup" "ML local theory setup" (Keyword.tag_ml Keyword.thy_decl)
  29.150 -    (Parse.ML_source >> IsarCmd.local_setup);
  29.151 +    (Parse.ML_source >> Isar_Cmd.local_setup);
  29.152  
  29.153  val _ =
  29.154    Outer_Syntax.command "attribute_setup" "define attribute in ML" (Keyword.tag_ml Keyword.thy_decl)
  29.155 @@ -357,14 +357,14 @@
  29.156  
  29.157  val _ =
  29.158    Outer_Syntax.local_theory "declaration" "generic ML declaration" (Keyword.tag_ml Keyword.thy_decl)
  29.159 -    (Parse.opt_keyword "pervasive" -- Parse.ML_source >> uncurry IsarCmd.declaration);
  29.160 +    (Parse.opt_keyword "pervasive" -- Parse.ML_source >> uncurry Isar_Cmd.declaration);
  29.161  
  29.162  val _ =
  29.163    Outer_Syntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)
  29.164      (Parse.name --
  29.165        (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")" --| Parse.$$$ "=") --
  29.166        Parse.ML_source -- Scan.optional (Parse.$$$ "identifier" |-- Scan.repeat1 Parse.xname) []
  29.167 -    >> (fn (((a, b), c), d) => IsarCmd.simproc_setup a b c d));
  29.168 +    >> (fn (((a, b), c), d) => Isar_Cmd.simproc_setup a b c d));
  29.169  
  29.170  
  29.171  (* translation functions *)
  29.172 @@ -374,27 +374,27 @@
  29.173  val _ =
  29.174    Outer_Syntax.command "parse_ast_translation" "install parse ast translation functions"
  29.175      (Keyword.tag_ml Keyword.thy_decl)
  29.176 -    (trfun >> (Toplevel.theory o IsarCmd.parse_ast_translation));
  29.177 +    (trfun >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
  29.178  
  29.179  val _ =
  29.180    Outer_Syntax.command "parse_translation" "install parse translation functions"
  29.181      (Keyword.tag_ml Keyword.thy_decl)
  29.182 -    (trfun >> (Toplevel.theory o IsarCmd.parse_translation));
  29.183 +    (trfun >> (Toplevel.theory o Isar_Cmd.parse_translation));
  29.184  
  29.185  val _ =
  29.186    Outer_Syntax.command "print_translation" "install print translation functions"
  29.187      (Keyword.tag_ml Keyword.thy_decl)
  29.188 -    (trfun >> (Toplevel.theory o IsarCmd.print_translation));
  29.189 +    (trfun >> (Toplevel.theory o Isar_Cmd.print_translation));
  29.190  
  29.191  val _ =
  29.192    Outer_Syntax.command "typed_print_translation" "install typed print translation functions"
  29.193      (Keyword.tag_ml Keyword.thy_decl)
  29.194 -    (trfun >> (Toplevel.theory o IsarCmd.typed_print_translation));
  29.195 +    (trfun >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
  29.196  
  29.197  val _ =
  29.198    Outer_Syntax.command "print_ast_translation" "install print ast translation functions"
  29.199      (Keyword.tag_ml Keyword.thy_decl)
  29.200 -    (trfun >> (Toplevel.theory o IsarCmd.print_ast_translation));
  29.201 +    (trfun >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
  29.202  
  29.203  
  29.204  (* oracles *)
  29.205 @@ -402,7 +402,7 @@
  29.206  val _ =
  29.207    Outer_Syntax.command "oracle" "declare oracle" (Keyword.tag_ml Keyword.thy_decl)
  29.208      (Parse.position Parse.name -- (Parse.$$$ "=" |-- Parse.ML_source) >>
  29.209 -      (fn (x, y) => Toplevel.theory (IsarCmd.oracle x y)));
  29.210 +      (fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
  29.211  
  29.212  
  29.213  (* local theories *)
  29.214 @@ -537,22 +537,22 @@
  29.215  val _ =
  29.216    Outer_Syntax.command "have" "state local goal"
  29.217      (Keyword.tag_proof Keyword.prf_goal)
  29.218 -    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
  29.219 +    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));
  29.220  
  29.221  val _ =
  29.222    Outer_Syntax.command "hence" "abbreviates \"then have\""
  29.223      (Keyword.tag_proof Keyword.prf_goal)
  29.224 -    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
  29.225 +    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.hence));
  29.226  
  29.227  val _ =
  29.228    Outer_Syntax.command "show" "state local goal, solving current obligation"
  29.229      (Keyword.tag_proof Keyword.prf_asm_goal)
  29.230 -    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
  29.231 +    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.show));
  29.232  
  29.233  val _ =
  29.234    Outer_Syntax.command "thus" "abbreviates \"then show\""
  29.235      (Keyword.tag_proof Keyword.prf_asm_goal)
  29.236 -    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
  29.237 +    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.thus));
  29.238  
  29.239  
  29.240  (* facts *)
  29.241 @@ -673,32 +673,32 @@
  29.242  val _ =
  29.243    Outer_Syntax.command "qed" "conclude (sub-)proof"
  29.244      (Keyword.tag_proof Keyword.qed_block)
  29.245 -    (Scan.option Method.parse >> IsarCmd.qed);
  29.246 +    (Scan.option Method.parse >> Isar_Cmd.qed);
  29.247  
  29.248  val _ =
  29.249    Outer_Syntax.command "by" "terminal backward proof"
  29.250      (Keyword.tag_proof Keyword.qed)
  29.251 -    (Method.parse -- Scan.option Method.parse >> IsarCmd.terminal_proof);
  29.252 +    (Method.parse -- Scan.option Method.parse >> Isar_Cmd.terminal_proof);
  29.253  
  29.254  val _ =
  29.255    Outer_Syntax.command ".." "default proof"
  29.256      (Keyword.tag_proof Keyword.qed)
  29.257 -    (Scan.succeed IsarCmd.default_proof);
  29.258 +    (Scan.succeed Isar_Cmd.default_proof);
  29.259  
  29.260  val _ =
  29.261    Outer_Syntax.command "." "immediate proof"
  29.262      (Keyword.tag_proof Keyword.qed)
  29.263 -    (Scan.succeed IsarCmd.immediate_proof);
  29.264 +    (Scan.succeed Isar_Cmd.immediate_proof);
  29.265  
  29.266  val _ =
  29.267    Outer_Syntax.command "done" "done proof"
  29.268      (Keyword.tag_proof Keyword.qed)
  29.269 -    (Scan.succeed IsarCmd.done_proof);
  29.270 +    (Scan.succeed Isar_Cmd.done_proof);
  29.271  
  29.272  val _ =
  29.273    Outer_Syntax.command "sorry" "skip proof (quick-and-dirty mode only!)"
  29.274      (Keyword.tag_proof Keyword.qed)
  29.275 -    (Scan.succeed IsarCmd.skip_proof);
  29.276 +    (Scan.succeed Isar_Cmd.skip_proof);
  29.277  
  29.278  val _ =
  29.279    Outer_Syntax.command "oops" "forget proof"
  29.280 @@ -796,7 +796,7 @@
  29.281  
  29.282  val _ =
  29.283    Outer_Syntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
  29.284 -    Keyword.diag (Parse.nat >> (Toplevel.no_timing oo IsarCmd.pretty_setmargin));
  29.285 +    Keyword.diag (Parse.nat >> (Toplevel.no_timing oo Isar_Cmd.pretty_setmargin));
  29.286  
  29.287  val _ =
  29.288    Outer_Syntax.improper_command "help" "print outer syntax commands" Keyword.diag
  29.289 @@ -808,32 +808,32 @@
  29.290  
  29.291  val _ =
  29.292    Outer_Syntax.improper_command "print_configs" "print configuration options" Keyword.diag
  29.293 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_configs));
  29.294 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_configs));
  29.295  
  29.296  val _ =
  29.297    Outer_Syntax.improper_command "print_context" "print theory context name" Keyword.diag
  29.298 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_context));
  29.299 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_context));
  29.300  
  29.301  val _ =
  29.302    Outer_Syntax.improper_command "print_theory" "print logical theory contents (verbose!)"
  29.303 -    Keyword.diag (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theory));
  29.304 +    Keyword.diag (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theory));
  29.305  
  29.306  val _ =
  29.307    Outer_Syntax.improper_command "print_syntax" "print inner syntax of context (verbose!)"
  29.308 -    Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_syntax));
  29.309 +    Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_syntax));
  29.310  
  29.311  val _ =
  29.312    Outer_Syntax.improper_command "print_abbrevs" "print constant abbreviation of context"
  29.313 -    Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.print_abbrevs));
  29.314 +    Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_abbrevs));
  29.315  
  29.316  val _ =
  29.317    Outer_Syntax.improper_command "print_theorems"
  29.318        "print theorems of local theory or proof context" Keyword.diag
  29.319 -    (opt_bang >> (Toplevel.no_timing oo IsarCmd.print_theorems));
  29.320 +    (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theorems));
  29.321  
  29.322  val _ =
  29.323    Outer_Syntax.improper_command "print_locales" "print locales of this theory" Keyword.diag
  29.324 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales));
  29.325 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_locales));
  29.326  
  29.327  val _ =
  29.328    Outer_Syntax.improper_command "print_classes" "print classes of this theory" Keyword.diag
  29.329 @@ -842,89 +842,89 @@
  29.330  
  29.331  val _ =
  29.332    Outer_Syntax.improper_command "print_locale" "print locale of this theory" Keyword.diag
  29.333 -    (opt_bang -- Parse.xname >> (Toplevel.no_timing oo IsarCmd.print_locale));
  29.334 +    (opt_bang -- Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_locale));
  29.335  
  29.336  val _ =
  29.337    Outer_Syntax.improper_command "print_interps"
  29.338      "print interpretations of locale for this theory" Keyword.diag
  29.339 -    (Parse.xname >> (Toplevel.no_timing oo IsarCmd.print_registrations));
  29.340 +    (Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
  29.341  
  29.342  val _ =
  29.343    Outer_Syntax.improper_command "print_attributes" "print attributes of this theory" Keyword.diag
  29.344 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_attributes));
  29.345 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_attributes));
  29.346  
  29.347  val _ =
  29.348    Outer_Syntax.improper_command "print_simpset" "print context of Simplifier" Keyword.diag
  29.349 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_simpset));
  29.350 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_simpset));
  29.351  
  29.352  val _ =
  29.353    Outer_Syntax.improper_command "print_rules" "print intro/elim rules" Keyword.diag
  29.354 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_rules));
  29.355 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_rules));
  29.356  
  29.357  val _ =
  29.358    Outer_Syntax.improper_command "print_trans_rules" "print transitivity rules" Keyword.diag
  29.359 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_trans_rules));
  29.360 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_trans_rules));
  29.361  
  29.362  val _ =
  29.363    Outer_Syntax.improper_command "print_methods" "print methods of this theory" Keyword.diag
  29.364 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_methods));
  29.365 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_methods));
  29.366  
  29.367  val _ =
  29.368    Outer_Syntax.improper_command "print_antiquotations" "print antiquotations (global)" Keyword.diag
  29.369 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
  29.370 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_antiquotations));
  29.371  
  29.372  val _ =
  29.373    Outer_Syntax.improper_command "thy_deps" "visualize theory dependencies"
  29.374 -    Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.thy_deps));
  29.375 +    Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.thy_deps));
  29.376  
  29.377  val _ =
  29.378    Outer_Syntax.improper_command "class_deps" "visualize class dependencies"
  29.379 -    Keyword.diag (Scan.succeed (Toplevel.no_timing o IsarCmd.class_deps));
  29.380 +    Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.class_deps));
  29.381  
  29.382  val _ =
  29.383    Outer_Syntax.improper_command "thm_deps" "visualize theorem dependencies"
  29.384 -    Keyword.diag (Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
  29.385 +    Keyword.diag (Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.thm_deps));
  29.386  
  29.387  val _ =
  29.388    Outer_Syntax.improper_command "print_binds" "print term bindings of proof context" Keyword.diag
  29.389 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_binds));
  29.390 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_binds));
  29.391  
  29.392  val _ =
  29.393    Outer_Syntax.improper_command "print_facts" "print facts of proof context" Keyword.diag
  29.394 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_facts));
  29.395 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_facts));
  29.396  
  29.397  val _ =
  29.398    Outer_Syntax.improper_command "print_cases" "print cases of proof context" Keyword.diag
  29.399 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.print_cases));
  29.400 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_cases));
  29.401  
  29.402  val _ =
  29.403    Outer_Syntax.improper_command "print_statement" "print theorems as long statements" Keyword.diag
  29.404 -    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts));
  29.405 +    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_stmts));
  29.406  
  29.407  val _ =
  29.408    Outer_Syntax.improper_command "thm" "print theorems" Keyword.diag
  29.409 -    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
  29.410 +    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_thms));
  29.411  
  29.412  val _ =
  29.413    Outer_Syntax.improper_command "prf" "print proof terms of theorems" Keyword.diag
  29.414      (opt_modes -- Scan.option Parse_Spec.xthms1
  29.415 -      >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
  29.416 +      >> (Toplevel.no_timing oo Isar_Cmd.print_prfs false));
  29.417  
  29.418  val _ =
  29.419    Outer_Syntax.improper_command "full_prf" "print full proof terms of theorems" Keyword.diag
  29.420 -    (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
  29.421 +    (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_prfs true));
  29.422  
  29.423  val _ =
  29.424    Outer_Syntax.improper_command "prop" "read and print proposition" Keyword.diag
  29.425 -    (opt_modes -- Parse.term >> (Toplevel.no_timing oo IsarCmd.print_prop));
  29.426 +    (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_prop));
  29.427  
  29.428  val _ =
  29.429    Outer_Syntax.improper_command "term" "read and print term" Keyword.diag
  29.430 -    (opt_modes -- Parse.term >> (Toplevel.no_timing oo IsarCmd.print_term));
  29.431 +    (opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_term));
  29.432  
  29.433  val _ =
  29.434    Outer_Syntax.improper_command "typ" "read and print type" Keyword.diag
  29.435 -    (opt_modes -- Parse.typ >> (Toplevel.no_timing oo IsarCmd.print_type));
  29.436 +    (opt_modes -- Parse.typ >> (Toplevel.no_timing oo Isar_Cmd.print_type));
  29.437  
  29.438  val _ =
  29.439    Outer_Syntax.improper_command "print_codesetup" "print code generator setup" Keyword.diag
  29.440 @@ -936,7 +936,7 @@
  29.441    Outer_Syntax.improper_command "unused_thms" "find unused theorems" Keyword.diag
  29.442      (Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
  29.443         Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >>
  29.444 -         (Toplevel.no_timing oo IsarCmd.unused_thms));
  29.445 +         (Toplevel.no_timing oo Isar_Cmd.unused_thms));
  29.446  
  29.447  
  29.448  
  29.449 @@ -944,54 +944,54 @@
  29.450  
  29.451  val _ =
  29.452    Outer_Syntax.improper_command "cd" "change current working directory" Keyword.diag
  29.453 -    (Parse.path >> (Toplevel.no_timing oo IsarCmd.cd));
  29.454 +    (Parse.path >> (Toplevel.no_timing oo Isar_Cmd.cd));
  29.455  
  29.456  val _ =
  29.457    Outer_Syntax.improper_command "pwd" "print current working directory" Keyword.diag
  29.458 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.pwd));
  29.459 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.pwd));
  29.460  
  29.461  val _ =
  29.462    Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.diag
  29.463      (Parse.name >> (fn name =>
  29.464 -      Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.use_thy name)));
  29.465 +      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.use_thy name)));
  29.466  
  29.467  val _ =
  29.468    Outer_Syntax.improper_command "touch_thy" "outdate theory, including descendants" Keyword.diag
  29.469      (Parse.name >> (fn name =>
  29.470 -      Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.touch_thy name)));
  29.471 +      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.touch_thy name)));
  29.472  
  29.473  val _ =
  29.474    Outer_Syntax.improper_command "remove_thy" "remove theory from loader database" Keyword.diag
  29.475      (Parse.name >> (fn name =>
  29.476 -      Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.remove_thy name)));
  29.477 +      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
  29.478  
  29.479  val _ =
  29.480    Outer_Syntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
  29.481      Keyword.diag (Parse.name >> (fn name =>
  29.482 -      Toplevel.no_timing o Toplevel.imperative (fn () => ThyInfo.kill_thy name)));
  29.483 +      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
  29.484  
  29.485  val _ =
  29.486    Outer_Syntax.improper_command "display_drafts" "display raw source files with symbols"
  29.487 -    Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo IsarCmd.display_drafts));
  29.488 +    Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.display_drafts));
  29.489  
  29.490  val _ =
  29.491    Outer_Syntax.improper_command "print_drafts" "print raw source files with symbols"
  29.492 -    Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo IsarCmd.print_drafts));
  29.493 +    Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));
  29.494  
  29.495  val opt_limits =
  29.496    Scan.option Parse.nat -- Scan.option (Parse.$$$ "," |-- Parse.!!! Parse.nat);
  29.497  
  29.498  val _ =
  29.499    Outer_Syntax.improper_command "pr" "print current proof state (if present)" Keyword.diag
  29.500 -    (opt_modes -- opt_limits >> (Toplevel.no_timing oo IsarCmd.pr));
  29.501 +    (opt_modes -- opt_limits >> (Toplevel.no_timing oo Isar_Cmd.pr));
  29.502  
  29.503  val _ =
  29.504    Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.diag
  29.505 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.disable_pr));
  29.506 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.disable_pr));
  29.507  
  29.508  val _ =
  29.509    Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.diag
  29.510 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.enable_pr));
  29.511 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.enable_pr));
  29.512  
  29.513  val _ =
  29.514    Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.diag
  29.515 @@ -999,11 +999,11 @@
  29.516  
  29.517  val _ =
  29.518    Outer_Syntax.improper_command "quit" "quit Isabelle" Keyword.control
  29.519 -    (Parse.opt_unit >> (Toplevel.no_timing oo K IsarCmd.quit));
  29.520 +    (Parse.opt_unit >> (Toplevel.no_timing oo K Isar_Cmd.quit));
  29.521  
  29.522  val _ =
  29.523    Outer_Syntax.improper_command "exit" "exit Isar loop" Keyword.control
  29.524 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.exit));
  29.525 +    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.exit));
  29.526  
  29.527  end;
  29.528  
    30.1 --- a/src/Pure/Isar/method.ML	Mon May 31 19:36:13 2010 +0200
    30.2 +++ b/src/Pure/Isar/method.ML	Mon May 31 21:06:57 2010 +0200
    30.3 @@ -271,15 +271,16 @@
    30.4  val intros_tac = gen_intros_tac ALLGOALS;
    30.5  val try_intros_tac = gen_intros_tac TRYALL;
    30.6  
    30.7 +
    30.8  (* ML tactics *)
    30.9  
   30.10 -structure TacticData = Proof_Data
   30.11 +structure ML_Tactic = Proof_Data
   30.12  (
   30.13    type T = thm list -> tactic;
   30.14    fun init _ = undefined;
   30.15  );
   30.16  
   30.17 -val set_tactic = TacticData.put;
   30.18 +val set_tactic = ML_Tactic.put;
   30.19  
   30.20  fun ml_tactic (txt, pos) ctxt =
   30.21    let
   30.22 @@ -287,7 +288,7 @@
   30.23        (ML_Context.expression pos
   30.24          "fun tactic (facts: thm list) : tactic"
   30.25          "Context.map_proof (Method.set_tactic tactic)" (ML_Lex.read pos txt));
   30.26 -  in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (TacticData.get ctxt') end;
   30.27 +  in Context.setmp_thread_data (SOME (Context.Proof ctxt)) (ML_Tactic.get ctxt') end;
   30.28  
   30.29  fun tactic txt ctxt = METHOD (ml_tactic txt ctxt);
   30.30  fun raw_tactic txt ctxt = RAW_METHOD (ml_tactic txt ctxt);
    31.1 --- a/src/Pure/Isar/object_logic.ML	Mon May 31 19:36:13 2010 +0200
    31.2 +++ b/src/Pure/Isar/object_logic.ML	Mon May 31 21:06:57 2010 +0200
    31.3 @@ -46,7 +46,7 @@
    31.4  fun make_data (base_sort, judgment, atomize_rulify) =
    31.5    Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify};
    31.6  
    31.7 -structure ObjectLogicData = Theory_Data
    31.8 +structure Data = Theory_Data
    31.9  (
   31.10    type T = data;
   31.11    val empty = make_data (NONE, NONE, ([], []));
   31.12 @@ -63,10 +63,10 @@
   31.13        (Thm.merge_thms (atomize1, atomize2), Thm.merge_thms (rulify1, rulify2)));
   31.14  );
   31.15  
   31.16 -fun map_data f = ObjectLogicData.map (fn (Data {base_sort, judgment, atomize_rulify}) =>
   31.17 +fun map_data f = Data.map (fn (Data {base_sort, judgment, atomize_rulify}) =>
   31.18    make_data (f (base_sort, judgment, atomize_rulify)));
   31.19  
   31.20 -fun get_data thy = ObjectLogicData.get thy |> (fn Data args => args);
   31.21 +fun get_data thy = Data.get thy |> (fn Data args => args);
   31.22  
   31.23  
   31.24  
    32.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon May 31 19:36:13 2010 +0200
    32.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon May 31 21:06:57 2010 +0200
    32.3 @@ -11,7 +11,7 @@
    32.4  sig
    32.5    val command: string -> string -> Keyword.T ->
    32.6      (Toplevel.transition -> Toplevel.transition) parser -> unit
    32.7 -  val markup_command: ThyOutput.markup -> string -> string -> Keyword.T ->
    32.8 +  val markup_command: Thy_Output.markup -> string -> string -> Keyword.T ->
    32.9      (Toplevel.transition -> Toplevel.transition) parser -> unit
   32.10    val improper_command: string -> string -> Keyword.T ->
   32.11      (Toplevel.transition -> Toplevel.transition) parser -> unit
   32.12 @@ -43,7 +43,7 @@
   32.13  
   32.14  datatype command = Command of
   32.15   {comment: string,
   32.16 -  markup: ThyOutput.markup option,
   32.17 +  markup: Thy_Output.markup option,
   32.18    int_only: bool,
   32.19    parse: (Toplevel.transition -> Toplevel.transition) parser};
   32.20  
   32.21 @@ -83,7 +83,7 @@
   32.22  local
   32.23  
   32.24  val global_commands = Unsynchronized.ref (Symtab.empty: command Symtab.table);
   32.25 -val global_markups = Unsynchronized.ref ([]: (string * ThyOutput.markup) list);
   32.26 +val global_markups = Unsynchronized.ref ([]: (string * Thy_Output.markup) list);
   32.27  
   32.28  fun change_commands f = CRITICAL (fn () =>
   32.29   (Unsynchronized.change global_commands f;
   32.30 @@ -235,9 +235,9 @@
   32.31  
   32.32  fun prepare_span commands span =
   32.33    let
   32.34 -    val range_pos = Position.encode_range (ThySyntax.span_range span);
   32.35 -    val toks = ThySyntax.span_content span;
   32.36 -    val _ = List.app ThySyntax.report_token toks;
   32.37 +    val range_pos = Position.encode_range (Thy_Syntax.span_range span);
   32.38 +    val toks = Thy_Syntax.span_content span;
   32.39 +    val _ = List.app Thy_Syntax.report_token toks;
   32.40    in
   32.41      (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
   32.42        [tr] => (tr, true)
   32.43 @@ -257,7 +257,7 @@
   32.44  
   32.45  fun prepare_command pos str =
   32.46    let val (lexs, commands) = get_syntax () in
   32.47 -    (case ThySyntax.parse_spans lexs pos str of
   32.48 +    (case Thy_Syntax.parse_spans lexs pos str of
   32.49        [span] => #1 (prepare_span commands span)
   32.50      | _ => Toplevel.malformed pos not_singleton)
   32.51    end;
   32.52 @@ -271,21 +271,21 @@
   32.53  
   32.54      val _ = Present.init_theory name;
   32.55  
   32.56 -    val toks = Source.exhausted (ThySyntax.token_source lexs pos (Source.of_list text));
   32.57 -    val spans = Source.exhaust (ThySyntax.span_source toks);
   32.58 -    val _ = List.app ThySyntax.report_span spans;
   32.59 -    val units = Source.exhaust (ThySyntax.unit_source (Source.of_list spans))
   32.60 +    val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_list text));
   32.61 +    val spans = Source.exhaust (Thy_Syntax.span_source toks);
   32.62 +    val _ = List.app Thy_Syntax.report_span spans;
   32.63 +    val units = Source.exhaust (Thy_Syntax.unit_source (Source.of_list spans))
   32.64        |> maps (prepare_unit commands);
   32.65  
   32.66      val _ = Present.theory_source name
   32.67 -      (fn () => HTML.html_mode (implode o map ThySyntax.present_span) spans);
   32.68 +      (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
   32.69  
   32.70      val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
   32.71      val results = cond_timeit time "" (fn () => Toplevel.excursion units);
   32.72      val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
   32.73  
   32.74      fun after_load () =
   32.75 -      ThyOutput.present_thy (#1 lexs) Keyword.command_tags is_markup (Lazy.force results) toks
   32.76 +      Thy_Output.present_thy (#1 lexs) Keyword.command_tags is_markup (Lazy.force results) toks
   32.77        |> Buffer.content
   32.78        |> Present.theory_output name;
   32.79    in after_load end;
    33.1 --- a/src/Pure/Isar/proof_context.ML	Mon May 31 19:36:13 2010 +0200
    33.2 +++ b/src/Pure/Isar/proof_context.ML	Mon May 31 21:06:57 2010 +0200
    33.3 @@ -193,7 +193,7 @@
    33.4  
    33.5  val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
    33.6  
    33.7 -structure ContextData = Proof_Data
    33.8 +structure Data = Proof_Data
    33.9  (
   33.10    type T = ctxt;
   33.11    fun init thy =
   33.12 @@ -202,10 +202,10 @@
   33.13        (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []);
   33.14  );
   33.15  
   33.16 -fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args);
   33.17 +fun rep_context ctxt = Data.get ctxt |> (fn Ctxt args => args);
   33.18  
   33.19  fun map_context f =
   33.20 -  ContextData.map (fn Ctxt {mode, naming, syntax, tsig, consts, facts, cases} =>
   33.21 +  Data.map (fn Ctxt {mode, naming, syntax, tsig, consts, facts, cases} =>
   33.22      make_ctxt (f (mode, naming, syntax, tsig, consts, facts, cases)));
   33.23  
   33.24  fun set_mode mode = map_context (fn (_, naming, syntax, tsig, consts, facts, cases) =>
    34.1 --- a/src/Pure/Isar/specification.ML	Mon May 31 19:36:13 2010 +0200
    34.2 +++ b/src/Pure/Isar/specification.ML	Mon May 31 21:06:57 2010 +0200
    34.3 @@ -361,7 +361,7 @@
    34.4              #2 #> pair ths);
    34.5        in ((prems, stmt, SOME facts), goal_ctxt) end);
    34.6  
    34.7 -structure TheoremHook = Generic_Data
    34.8 +structure Theorem_Hook = Generic_Data
    34.9  (
   34.10    type T = ((bool -> Proof.state -> Proof.state) * stamp) list;
   34.11    val empty = [];
   34.12 @@ -407,7 +407,7 @@
   34.13      |> (case facts of NONE => I | SOME ths => Proof.refine_insert ths)
   34.14      |> tap (fn state => not schematic andalso Proof.schematic_goal state andalso
   34.15          error "Illegal schematic goal statement")
   34.16 -    |> Library.apply (map (fn (f, _) => f int) (rev (TheoremHook.get (Context.Proof goal_ctxt))))
   34.17 +    |> Library.apply (map (fn (f, _) => f int) (rev (Theorem_Hook.get (Context.Proof goal_ctxt))))
   34.18    end;
   34.19  
   34.20  in
   34.21 @@ -418,7 +418,7 @@
   34.22  val schematic_theorem = gen_theorem true (K I) Expression.cert_statement;
   34.23  val schematic_theorem_cmd = gen_theorem true Attrib.intern_src Expression.read_statement;
   34.24  
   34.25 -fun add_theorem_hook f = TheoremHook.map (cons (f, stamp ()));
   34.26 +fun add_theorem_hook f = Theorem_Hook.map (cons (f, stamp ()));
   34.27  
   34.28  end;
   34.29  
    35.1 --- a/src/Pure/Isar/toplevel.ML	Mon May 31 19:36:13 2010 +0200
    35.2 +++ b/src/Pure/Isar/toplevel.ML	Mon May 31 21:06:57 2010 +0200
    35.3 @@ -238,7 +238,7 @@
    35.4          |> Runtime.debugging
    35.5          |> Runtime.toplevel_error
    35.6            (fn exn => priority ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
    35.7 -      SimpleThread.attributes interrupts);
    35.8 +      Simple_Thread.attributes interrupts);
    35.9  
   35.10  
   35.11  (* node transactions -- maintaining stable checkpoints *)
   35.12 @@ -638,7 +638,7 @@
   35.13  fun run_command thy_name tr st =
   35.14    (case
   35.15        (case init_of tr of
   35.16 -        SOME name => Exn.capture (fn () => ThyLoad.check_name thy_name name) ()
   35.17 +        SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
   35.18        | NONE => Exn.Result ()) of
   35.19      Exn.Result () =>
   35.20        (case transition true tr st of
    36.1 --- a/src/Pure/ML/ml_antiquote.ML	Mon May 31 19:36:13 2010 +0200
    36.2 +++ b/src/Pure/ML/ml_antiquote.ML	Mon May 31 21:06:57 2010 +0200
    36.3 @@ -20,7 +20,7 @@
    36.4  
    36.5  (* ML names *)
    36.6  
    36.7 -structure NamesData = Proof_Data
    36.8 +structure Names = Proof_Data
    36.9  (
   36.10    type T = Name.context;
   36.11    fun init _ = ML_Syntax.reserved;
   36.12 @@ -28,9 +28,9 @@
   36.13  
   36.14  fun variant a ctxt =
   36.15    let
   36.16 -    val names = NamesData.get ctxt;
   36.17 +    val names = Names.get ctxt;
   36.18      val ([b], names') = Name.variants [a] names;
   36.19 -    val ctxt' = NamesData.put names' ctxt;
   36.20 +    val ctxt' = Names.put names' ctxt;
   36.21    in (b, ctxt') end;
   36.22  
   36.23  
   36.24 @@ -64,12 +64,12 @@
   36.25      >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name)));
   36.26  
   36.27  val _ = value "theory"
   36.28 -  (Scan.lift Args.name >> (fn name => "ThyInfo.get_theory " ^ ML_Syntax.print_string name)
   36.29 +  (Scan.lift Args.name >> (fn name => "Thy_Info.get_theory " ^ ML_Syntax.print_string name)
   36.30    || Scan.succeed "ML_Context.the_global_context ()");
   36.31  
   36.32  val _ = value "theory_ref"
   36.33    (Scan.lift Args.name >> (fn name =>
   36.34 -    "Theory.check_thy (ThyInfo.theory " ^ ML_Syntax.print_string name ^ ")")
   36.35 +    "Theory.check_thy (Thy_Info.theory " ^ ML_Syntax.print_string name ^ ")")
   36.36    || Scan.succeed "Theory.check_thy (ML_Context.the_global_context ())");
   36.37  
   36.38  val _ = value "context" (Scan.succeed "ML_Context.the_local_context ()");
    37.1 --- a/src/Pure/ML/ml_thms.ML	Mon May 31 19:36:13 2010 +0200
    37.2 +++ b/src/Pure/ML/ml_thms.ML	Mon May 31 21:06:57 2010 +0200
    37.3 @@ -15,15 +15,15 @@
    37.4  
    37.5  (* auxiliary facts table *)
    37.6  
    37.7 -structure AuxFacts = Proof_Data
    37.8 +structure Aux_Facts = Proof_Data
    37.9  (
   37.10    type T = thm list Inttab.table;
   37.11    fun init _ = Inttab.empty;
   37.12  );
   37.13  
   37.14 -val put_thms = AuxFacts.map o Inttab.update;
   37.15 +val put_thms = Aux_Facts.map o Inttab.update;
   37.16  
   37.17 -fun the_thms ctxt name = the (Inttab.lookup (AuxFacts.get ctxt) name);
   37.18 +fun the_thms ctxt name = the (Inttab.lookup (Aux_Facts.get ctxt) name);
   37.19  fun the_thm ctxt name = the_single (the_thms ctxt name);
   37.20  
   37.21  fun thm_bind kind a i =
    38.1 --- a/src/Pure/ProofGeneral/pgip_isabelle.ML	Mon May 31 19:36:13 2010 +0200
    38.2 +++ b/src/Pure/ProofGeneral/pgip_isabelle.ML	Mon May 31 21:06:57 2010 +0200
    38.3 @@ -80,7 +80,7 @@
    38.4                 NONE => (NONE, NONE)
    38.5               | SOME fname =>
    38.6                 let val path = Path.explode fname in
    38.7 -                 case ThyLoad.check_file Path.current path of
    38.8 +                 case Thy_Load.check_file Path.current path of
    38.9                     SOME _ => (SOME (PgipTypes.pgipurl_of_path path), NONE)
   38.10                   | NONE => (NONE, SOME fname)
   38.11                 end);
    39.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML	Mon May 31 19:36:13 2010 +0200
    39.2 +++ b/src/Pure/ProofGeneral/pgip_parser.ML	Mon May 31 21:06:57 2010 +0200
    39.3 @@ -91,18 +91,18 @@
    39.4  
    39.5  fun parse_span span =
    39.6    let
    39.7 -    val kind = ThySyntax.span_kind span;
    39.8 -    val toks = ThySyntax.span_content span;
    39.9 -    val text = implode (map (Print_Mode.setmp [] ThySyntax.present_token) toks);
   39.10 +    val kind = Thy_Syntax.span_kind span;
   39.11 +    val toks = Thy_Syntax.span_content span;
   39.12 +    val text = implode (map (Print_Mode.setmp [] Thy_Syntax.present_token) toks);
   39.13    in
   39.14      (case kind of
   39.15 -      ThySyntax.Command name => parse_command name text
   39.16 -    | ThySyntax.Ignored => [D.Whitespace {text = text}]
   39.17 -    | ThySyntax.Malformed => [D.Unparseable {text = text}])
   39.18 +      Thy_Syntax.Command name => parse_command name text
   39.19 +    | Thy_Syntax.Ignored => [D.Whitespace {text = text}]
   39.20 +    | Thy_Syntax.Malformed => [D.Unparseable {text = text}])
   39.21    end;
   39.22  
   39.23  
   39.24  fun pgip_parser pos str =
   39.25 -  maps parse_span (ThySyntax.parse_spans (Keyword.get_lexicons ()) pos str);
   39.26 +  maps parse_span (Thy_Syntax.parse_spans (Keyword.get_lexicons ()) pos str);
   39.27  
   39.28  end;
    40.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon May 31 19:36:13 2010 +0200
    40.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon May 31 21:06:57 2010 +0200
    40.3 @@ -113,15 +113,15 @@
    40.4  local
    40.5  
    40.6  fun trace_action action name =
    40.7 -  if action = ThyInfo.Update then
    40.8 -    List.app tell_file_loaded (ThyInfo.loaded_files name)
    40.9 -  else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
   40.10 -    List.app tell_file_retracted (ThyInfo.loaded_files name)
   40.11 +  if action = Thy_Info.Update then
   40.12 +    List.app tell_file_loaded (Thy_Info.loaded_files name)
   40.13 +  else if action = Thy_Info.Outdate orelse action = Thy_Info.Remove then
   40.14 +    List.app tell_file_retracted (Thy_Info.loaded_files name)
   40.15    else ();
   40.16  
   40.17  in
   40.18 -  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
   40.19 -  fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.get_names ());
   40.20 +  fun setup_thy_loader () = Thy_Info.add_hook trace_action;
   40.21 +  fun sync_thy_loader () = List.app (trace_action Thy_Info.Update) (Thy_Info.get_names ());
   40.22  end;
   40.23  
   40.24  
   40.25 @@ -130,19 +130,19 @@
   40.26  (*liberal low-level version*)
   40.27  val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/";
   40.28  
   40.29 -val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
   40.30 +val inform_file_retracted = Thy_Info.if_known_thy Thy_Info.remove_thy o thy_name;
   40.31  
   40.32  fun inform_file_processed file =
   40.33    let
   40.34      val name = thy_name file;
   40.35      val _ = name = "" andalso error ("Bad file name: " ^ quote file);
   40.36      val _ =
   40.37 -      if ThyInfo.check_known_thy name then
   40.38 +      if Thy_Info.check_known_thy name then
   40.39          (Isar.>> (Toplevel.commit_exit Position.none);
   40.40 -            ThyInfo.touch_child_thys name; ThyInfo.register_thy name)
   40.41 +            Thy_Info.touch_child_thys name; Thy_Info.register_thy name)
   40.42            handle ERROR msg =>
   40.43              (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
   40.44 -              tell_file_retracted (ThyLoad.thy_path name))
   40.45 +              tell_file_retracted (Thy_Load.thy_path name))
   40.46        else ();
   40.47      val _ = Isar.init ();
   40.48    in () end;
    41.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon May 31 19:36:13 2010 +0200
    41.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon May 31 21:06:57 2010 +0200
    41.3 @@ -198,18 +198,18 @@
    41.4        operations).
    41.5     *)
    41.6  fun trace_action action name =
    41.7 -  if action = ThyInfo.Update then
    41.8 -    List.app (tell_file_loaded true) (ThyInfo.loaded_files name)
    41.9 -  else if action = ThyInfo.Outdate then
   41.10 -    List.app (tell_file_outdated true) (ThyInfo.loaded_files name)
   41.11 -  else if action = ThyInfo.Remove then
   41.12 -      List.app (tell_file_retracted true) (ThyInfo.loaded_files name)
   41.13 +  if action = Thy_Info.Update then
   41.14 +    List.app (tell_file_loaded true) (Thy_Info.loaded_files name)
   41.15 +  else if action = Thy_Info.Outdate then
   41.16 +    List.app (tell_file_outdated true) (Thy_Info.loaded_files name)
   41.17 +  else if action = Thy_Info.Remove then
   41.18 +      List.app (tell_file_retracted true) (Thy_Info.loaded_files name)
   41.19    else ()
   41.20  
   41.21  
   41.22  in
   41.23 -  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
   41.24 -  fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.get_names ());
   41.25 +  fun setup_thy_loader () = Thy_Info.add_hook trace_action;
   41.26 +  fun sync_thy_loader () = List.app (trace_action Thy_Info.Update) (Thy_Info.get_names ());
   41.27  end;
   41.28  
   41.29  
   41.30 @@ -217,14 +217,14 @@
   41.31  
   41.32  val thy_name = Path.implode o #1 o Path.split_ext o Path.base;
   41.33  
   41.34 -val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
   41.35 -val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
   41.36 +val inform_file_retracted = Thy_Info.if_known_thy Thy_Info.remove_thy o thy_name;
   41.37 +val inform_file_processed = Thy_Info.if_known_thy Thy_Info.touch_child_thys o thy_name;
   41.38  
   41.39  fun proper_inform_file_processed path state =
   41.40    let val name = thy_name path in
   41.41 -    if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
   41.42 -     (ThyInfo.touch_child_thys name;
   41.43 -      ThyInfo.register_thy name handle ERROR msg =>
   41.44 +    if Toplevel.is_toplevel state andalso Thy_Info.known_thy name then
   41.45 +     (Thy_Info.touch_child_thys name;
   41.46 +      Thy_Info.register_thy name handle ERROR msg =>
   41.47         (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
   41.48          tell_file_retracted true (Path.base path)))
   41.49      else raise Toplevel.UNDEF
   41.50 @@ -522,7 +522,7 @@
   41.51  local
   41.52  
   41.53  fun theory_facts name =
   41.54 -  let val thy = ThyInfo.get_theory name
   41.55 +  let val thy = Thy_Info.get_theory name
   41.56    in (map PureThy.facts_of (Theory.parents_of thy), PureThy.facts_of thy) end;
   41.57  
   41.58  fun thms_of_thy name = map fst (theory_facts name |-> Facts.extern_static);
   41.59 @@ -556,13 +556,13 @@
   41.60      in
   41.61          case (thyname,objtype) of
   41.62             (NONE, NONE) =>
   41.63 -           setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
   41.64 +           setids (idtable ObjFile NONE (Thy_Info.get_names())) (*FIXME: uris*)
   41.65           | (NONE, SOME ObjFile) =>
   41.66 -           setids (idtable ObjFile NONE (ThyInfo.get_names())) (*FIXME: uris*)
   41.67 +           setids (idtable ObjFile NONE (Thy_Info.get_names())) (*FIXME: uris*)
   41.68           | (SOME fi, SOME ObjFile) =>
   41.69             setids (idtable ObjTheory (SOME fi) [fi])       (* TODO: check exists *)
   41.70           | (NONE, SOME ObjTheory) =>
   41.71 -           setids (idtable ObjTheory NONE (ThyInfo.get_names()))
   41.72 +           setids (idtable ObjTheory NONE (Thy_Info.get_names()))
   41.73           | (SOME thy, SOME ObjTheory) =>
   41.74             setids (idtable ObjTheory (SOME thy) (subthys_of_thy thy))
   41.75           | (SOME thy, SOME ObjTheorem) =>
   41.76 @@ -571,9 +571,9 @@
   41.77             (* A large query, but not unreasonable. ~5000 results for HOL.*)
   41.78             (* Several setids should be allowed, but Eclipse code is currently broken:
   41.79                List.app (fn thy => setids (idtable ObjTheorem (SOME thy) (subthms_of_thy thy)))
   41.80 -                         (ThyInfo.get_names()) *)
   41.81 +                         (Thy_Info.get_names()) *)
   41.82             setids (idtable ObjTheorem NONE (* this one gives ~7000 for HOL *)
   41.83 -                           (maps qualified_thms_of_thy (ThyInfo.get_names())))
   41.84 +                           (maps qualified_thms_of_thy (Thy_Info.get_names())))
   41.85           | _ => warning ("askids: ignored argument combination")
   41.86      end
   41.87  
   41.88 @@ -592,14 +592,14 @@
   41.89  
   41.90          fun filerefs f =
   41.91              let val thy = thy_name f
   41.92 -                val filerefs = #uses (ThyLoad.deps_thy (Path.dir f) thy)
   41.93 +                val filerefs = #uses (Thy_Load.deps_thy (Path.dir f) thy)
   41.94              in
   41.95                  issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
   41.96                                       name=NONE, idtables=[], fileurls=filerefs})
   41.97              end
   41.98  
   41.99          fun thyrefs thy =
  41.100 -            let val thyrefs = #imports (ThyLoad.deps_thy Path.current thy)
  41.101 +            let val thyrefs = #imports (Thy_Load.deps_thy Path.current thy)
  41.102              in
  41.103                  issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
  41.104                                       name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,
  41.105 @@ -642,7 +642,7 @@
  41.106          fun splitthy id =
  41.107              let val comps = Long_Name.explode id
  41.108              in case comps of
  41.109 -                   (thy::(rest as _::_)) => (ThyInfo.get_theory thy, space_implode "." rest)
  41.110 +                   (thy::(rest as _::_)) => (Thy_Info.get_theory thy, space_implode "." rest)
  41.111                   | [plainid] => (topthy(),plainid)
  41.112                   | _ => raise Toplevel.UNDEF (* assert false *)
  41.113              end
  41.114 @@ -659,8 +659,8 @@
  41.115          val string_of_thy = Pretty.string_of o Proof_Display.pretty_full_theory false
  41.116      in
  41.117          case (thyname, objtype) of
  41.118 -            (_, ObjTheory) => idvalue [string_of_thy (ThyInfo.get_theory name)]
  41.119 -          | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (ThyInfo.get_theory thy, name))
  41.120 +            (_, ObjTheory) => idvalue [string_of_thy (Thy_Info.get_theory name)]
  41.121 +          | (SOME thy, ObjTheorem) => idvalue (strings_of_thm (Thy_Info.get_theory thy, name))
  41.122            | (NONE, ObjTheorem) => idvalue (strings_of_thm (splitthy name))
  41.123            | (_, ot) => error ("Cannot show objects of type "^(PgipTypes.name_of_objtype ot))
  41.124      end
  41.125 @@ -785,8 +785,8 @@
  41.126     in
  41.127         (case (!current_working_dir) of
  41.128              NONE => ()
  41.129 -          | SOME dir => ThyLoad.del_path dir;
  41.130 -        ThyLoad.add_path newdir;
  41.131 +          | SOME dir => Thy_Load.del_path dir;
  41.132 +        Thy_Load.add_path newdir;
  41.133          current_working_dir := SOME newdir)
  41.134     end
  41.135  end
  41.136 @@ -806,7 +806,7 @@
  41.137        val filedir = Path.dir filepath
  41.138        val thy_name = Path.implode o #1 o Path.split_ext o Path.base
  41.139        val openfile_retract = Output.no_warnings_CRITICAL
  41.140 -        (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
  41.141 +        (Thy_Info.if_known_thy Thy_Info.remove_thy) o thy_name;
  41.142    in
  41.143        case !currently_open_file of
  41.144            SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
  41.145 @@ -856,7 +856,7 @@
  41.146                       (* TODO: next should be in thy loader, here just for testing *)
  41.147                       let
  41.148                           val name = thy_name url
  41.149 -                     in List.app (tell_file_retracted false) (ThyInfo.loaded_files name) end;
  41.150 +                     in List.app (tell_file_retracted false) (Thy_Info.loaded_files name) end;
  41.151                       inform_file_retracted url)
  41.152      end
  41.153  
    42.1 --- a/src/Pure/ROOT.ML	Mon May 31 19:36:13 2010 +0200
    42.2 +++ b/src/Pure/ROOT.ML	Mon May 31 21:06:57 2010 +0200
    42.3 @@ -299,18 +299,15 @@
    42.4  struct
    42.5  
    42.6  structure OuterKeyword = Keyword;
    42.7 -
    42.8 -structure OuterLex =
    42.9 -struct
   42.10 -  open Token;
   42.11 -  type token = T;
   42.12 -end;
   42.13 -
   42.14 +structure OuterLex = struct open Token type token = T end;
   42.15  structure OuterParse = Parse;
   42.16  structure OuterSyntax = Outer_Syntax;
   42.17 +structure PrintMode = Print_Mode;
   42.18  structure SpecParse = Parse_Spec;
   42.19 +structure ThyInfo = Thy_Info;
   42.20 +structure ThyLoad = Thy_Load;
   42.21 +structure ThyOutput = Thy_Output;
   42.22  structure TypeInfer = Type_Infer;
   42.23 -structure PrintMode = Print_Mode;
   42.24  
   42.25  end;
   42.26  
    43.1 --- a/src/Pure/Syntax/mixfix.ML	Mon May 31 19:36:13 2010 +0200
    43.2 +++ b/src/Pure/Syntax/mixfix.ML	Mon May 31 21:06:57 2010 +0200
    43.3 @@ -31,8 +31,8 @@
    43.4  signature MIXFIX =
    43.5  sig
    43.6    include MIXFIX1
    43.7 -  val syn_ext_types: (string * typ * mixfix) list -> SynExt.syn_ext
    43.8 -  val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> SynExt.syn_ext
    43.9 +  val syn_ext_types: (string * typ * mixfix) list -> Syn_Ext.syn_ext
   43.10 +  val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> Syn_Ext.syn_ext
   43.11  end;
   43.12  
   43.13  structure Mixfix: MIXFIX =
   43.14 @@ -83,11 +83,11 @@
   43.15  (* syntax specifications *)
   43.16  
   43.17  fun mixfix_args NoSyn = 0
   43.18 -  | mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy
   43.19 -  | mixfix_args (Delimfix sy) = SynExt.mfix_args sy
   43.20 -  | mixfix_args (Infix (sy, _)) = 2 + SynExt.mfix_args sy
   43.21 -  | mixfix_args (Infixl (sy, _)) = 2 + SynExt.mfix_args sy
   43.22 -  | mixfix_args (Infixr (sy, _)) = 2 + SynExt.mfix_args sy
   43.23 +  | mixfix_args (Mixfix (sy, _, _)) = Syn_Ext.mfix_args sy
   43.24 +  | mixfix_args (Delimfix sy) = Syn_Ext.mfix_args sy
   43.25 +  | mixfix_args (Infix (sy, _)) = 2 + Syn_Ext.mfix_args sy
   43.26 +  | mixfix_args (Infixl (sy, _)) = 2 + Syn_Ext.mfix_args sy
   43.27 +  | mixfix_args (Infixr (sy, _)) = 2 + Syn_Ext.mfix_args sy
   43.28    | mixfix_args (Binder _) = 1
   43.29    | mixfix_args Structure = 0;
   43.30  
   43.31 @@ -97,29 +97,29 @@
   43.32  
   43.33  (* syn_ext_types *)
   43.34  
   43.35 -fun make_type n = replicate n SynExt.typeT ---> SynExt.typeT;
   43.36 +fun make_type n = replicate n Syn_Ext.typeT ---> Syn_Ext.typeT;
   43.37  
   43.38  fun syn_ext_types type_decls =
   43.39    let
   43.40 -    fun mk_infix sy ty t p1 p2 p3 = SynExt.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3);
   43.41 +    fun mk_infix sy ty t p1 p2 p3 = Syn_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, t, [p1, p2], p3);
   43.42  
   43.43      fun mfix_of (_, _, NoSyn) = NONE
   43.44 -      | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (SynExt.Mfix (sy, ty, t, ps, p))
   43.45 -      | mfix_of (t, ty, Delimfix sy) = SOME (SynExt.Mfix (sy, ty, t, [], SynExt.max_pri))
   43.46 +      | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syn_Ext.Mfix (sy, ty, t, ps, p))
   43.47 +      | mfix_of (t, ty, Delimfix sy) = SOME (Syn_Ext.Mfix (sy, ty, t, [], Syn_Ext.max_pri))
   43.48        | mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
   43.49        | mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p)
   43.50        | mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p)
   43.51        | mfix_of (t, _, _) = error ("Bad mixfix declaration for " ^ quote t);  (* FIXME printable t (!?) *)
   43.52  
   43.53 -    fun check_args (_, ty, _) (SOME (mfix as SynExt.Mfix (sy, _, _, _, _))) =
   43.54 -          if length (Term.binder_types ty) = SynExt.mfix_args sy then ()
   43.55 -          else SynExt.err_in_mfix "Bad number of type constructor arguments" mfix
   43.56 +    fun check_args (_, ty, _) (SOME (mfix as Syn_Ext.Mfix (sy, _, _, _, _))) =
   43.57 +          if length (Term.binder_types ty) = Syn_Ext.mfix_args sy then ()
   43.58 +          else Syn_Ext.err_in_mfix "Bad number of type constructor arguments" mfix
   43.59        | check_args _ NONE = ();
   43.60  
   43.61      val mfix = map mfix_of type_decls;
   43.62      val _ = map2 check_args type_decls mfix;
   43.63      val xconsts = map #1 type_decls;
   43.64 -  in SynExt.syn_ext (map_filter I mfix) xconsts ([], [], [], []) [] ([], []) end;
   43.65 +  in Syn_Ext.syn_ext (map_filter I mfix) xconsts ([], [], [], []) [] ([], []) end;
   43.66  
   43.67  
   43.68  (* syn_ext_consts *)
   43.69 @@ -130,21 +130,21 @@
   43.70  fun syn_ext_consts is_logtype const_decls =
   43.71    let
   43.72      fun mk_infix sy ty c p1 p2 p3 =
   43.73 -      [SynExt.Mfix ("op " ^ sy, ty, c, [], SynExt.max_pri),
   43.74 -       SynExt.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
   43.75 +      [Syn_Ext.Mfix ("op " ^ sy, ty, c, [], Syn_Ext.max_pri),
   43.76 +       Syn_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
   43.77  
   43.78      fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
   43.79            [Type ("idts", []), ty2] ---> ty3
   43.80        | binder_typ c _ = error ("Bad type of binder: " ^ quote c);
   43.81  
   43.82      fun mfix_of (_, _, NoSyn) = []
   43.83 -      | mfix_of (c, ty, Mixfix (sy, ps, p)) = [SynExt.Mfix (sy, ty, c, ps, p)]
   43.84 -      | mfix_of (c, ty, Delimfix sy) = [SynExt.Mfix (sy, ty, c, [], SynExt.max_pri)]
   43.85 +      | mfix_of (c, ty, Mixfix (sy, ps, p)) = [Syn_Ext.Mfix (sy, ty, c, ps, p)]
   43.86 +      | mfix_of (c, ty, Delimfix sy) = [Syn_Ext.Mfix (sy, ty, c, [], Syn_Ext.max_pri)]
   43.87        | mfix_of (c, ty, Infix (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p
   43.88        | mfix_of (c, ty, Infixl (sy, p)) = mk_infix sy ty c p (p + 1) p
   43.89        | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p
   43.90        | mfix_of (c, ty, Binder (sy, p, q)) =
   43.91 -          [SynExt.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
   43.92 +          [Syn_Ext.Mfix ("(3" ^ sy ^ "_./ _)", binder_typ c ty, (binder_name c), [0, p], q)]
   43.93        | mfix_of (c, _, _) = error ("Bad mixfix declaration for " ^ quote c);   (* FIXME printable c (!?) *)
   43.94  
   43.95      fun binder (c, _, Binder _) = SOME (binder_name c, c)
   43.96 @@ -154,12 +154,12 @@
   43.97      val xconsts = map #1 const_decls;
   43.98      val binders = map_filter binder const_decls;
   43.99      val binder_trs = binders
  43.100 -      |> map (SynExt.stamp_trfun binder_stamp o apsnd K o SynTrans.mk_binder_tr);
  43.101 +      |> map (Syn_Ext.stamp_trfun binder_stamp o apsnd K o Syn_Trans.mk_binder_tr);
  43.102      val binder_trs' = binders
  43.103 -      |> map (SynExt.stamp_trfun binder_stamp o
  43.104 -          apsnd (K o SynTrans.non_typed_tr') o SynTrans.mk_binder_tr' o swap);
  43.105 +      |> map (Syn_Ext.stamp_trfun binder_stamp o
  43.106 +          apsnd (K o Syn_Trans.non_typed_tr') o Syn_Trans.mk_binder_tr' o swap);
  43.107    in
  43.108 -    SynExt.syn_ext' true is_logtype
  43.109 +    Syn_Ext.syn_ext' true is_logtype
  43.110        mfix xconsts ([], binder_trs, binder_trs', []) [] ([], [])
  43.111    end;
  43.112  
    44.1 --- a/src/Pure/Syntax/parser.ML	Mon May 31 19:36:13 2010 +0200
    44.2 +++ b/src/Pure/Syntax/parser.ML	Mon May 31 21:06:57 2010 +0200
    44.3 @@ -8,8 +8,8 @@
    44.4  sig
    44.5    type gram
    44.6    val empty_gram: gram
    44.7 -  val extend_gram: gram -> SynExt.xprod list -> gram
    44.8 -  val make_gram: SynExt.xprod list -> gram
    44.9 +  val extend_gram: gram -> Syn_Ext.xprod list -> gram
   44.10 +  val make_gram: Syn_Ext.xprod list -> gram
   44.11    val merge_grams: gram -> gram -> gram
   44.12    val pretty_gram: gram -> Pretty.T list
   44.13    datatype parsetree =
   44.14 @@ -23,7 +23,7 @@
   44.15  structure Parser: PARSER =
   44.16  struct
   44.17  
   44.18 -open Lexicon SynExt;
   44.19 +open Lexicon Syn_Ext;
   44.20  
   44.21  
   44.22  (** datatype gram **)
    45.1 --- a/src/Pure/Syntax/printer.ML	Mon May 31 19:36:13 2010 +0200
    45.2 +++ b/src/Pure/Syntax/printer.ML	Mon May 31 21:06:57 2010 +0200
    45.3 @@ -26,8 +26,8 @@
    45.4      (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
    45.5    type prtabs
    45.6    val empty_prtabs: prtabs
    45.7 -  val update_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
    45.8 -  val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
    45.9 +  val update_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs
   45.10 +  val remove_prtabs: string -> Syn_Ext.xprod list -> prtabs -> prtabs
   45.11    val merge_prtabs: prtabs -> prtabs -> prtabs
   45.12    val pretty_term_ast: {extern_class: string -> xstring, extern_type: string -> xstring,
   45.13        extern_const: string -> xstring} -> Proof.context -> bool -> prtabs ->
   45.14 @@ -101,8 +101,8 @@
   45.15          handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
   45.16    in ast_of tm end;
   45.17  
   45.18 -fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (TypeExt.term_of_sort S);
   45.19 -fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (TypeExt.term_of_typ (! show_sorts) T);
   45.20 +fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (Type_Ext.term_of_sort S);
   45.21 +fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (Type_Ext.term_of_typ (! show_sorts) T);
   45.22  
   45.23  
   45.24  
   45.25 @@ -114,7 +114,7 @@
   45.26      val {structs, fixes} = idents;
   45.27  
   45.28      fun mark_atoms ((t as Const (c, T)) $ u) =
   45.29 -          if member (op =) SynExt.standard_token_markers c
   45.30 +          if member (op =) Syn_Ext.standard_token_markers c
   45.31            then t $ u else mark_atoms t $ mark_atoms u
   45.32        | mark_atoms (t $ u) = mark_atoms t $ mark_atoms u
   45.33        | mark_atoms (Abs (x, T, t)) = Abs (x, T, mark_atoms t)
   45.34 @@ -130,7 +130,7 @@
   45.35              else Lexicon.const "_free" $ t
   45.36            end
   45.37        | mark_atoms (t as Var (xi, T)) =
   45.38 -          if xi = SynExt.dddot_indexname then Const ("_DDDOT", T)
   45.39 +          if xi = Syn_Ext.dddot_indexname then Const ("_DDDOT", T)
   45.40            else Lexicon.const "_var" $ t
   45.41        | mark_atoms a = a;
   45.42  
   45.43 @@ -155,7 +155,7 @@
   45.44  
   45.45      fun ast_of tm =
   45.46        (case strip_comb tm of
   45.47 -        (t as Abs _, ts) => Ast.mk_appl (ast_of (SynTrans.abs_tr' t)) (map ast_of ts)
   45.48 +        (t as Abs _, ts) => Ast.mk_appl (ast_of (Syn_Trans.abs_tr' t)) (map ast_of ts)
   45.49        | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
   45.50            Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
   45.51        | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
   45.52 @@ -176,12 +176,12 @@
   45.53  
   45.54      and constrain t T =
   45.55        if show_types andalso T <> dummyT then
   45.56 -        Ast.Appl [Ast.Constant SynExt.constrainC, simple_ast_of t,
   45.57 -          ast_of_termT ctxt trf (TypeExt.term_of_typ show_sorts T)]
   45.58 +        Ast.Appl [Ast.Constant Syn_Ext.constrainC, simple_ast_of t,
   45.59 +          ast_of_termT ctxt trf (Type_Ext.term_of_typ show_sorts T)]
   45.60        else simple_ast_of t;
   45.61    in
   45.62      tm
   45.63 -    |> SynTrans.prop_tr'
   45.64 +    |> Syn_Trans.prop_tr'
   45.65      |> show_types ? (#1 o prune_typs o rpair [])
   45.66      |> mark_atoms
   45.67      |> ast_of
   45.68 @@ -211,29 +211,29 @@
   45.69  
   45.70  (* xprod_to_fmt *)
   45.71  
   45.72 -fun xprod_to_fmt (SynExt.XProd (_, _, "", _)) = NONE
   45.73 -  | xprod_to_fmt (SynExt.XProd (_, xsymbs, const, pri)) =
   45.74 +fun xprod_to_fmt (Syn_Ext.XProd (_, _, "", _)) = NONE
   45.75 +  | xprod_to_fmt (Syn_Ext.XProd (_, xsymbs, const, pri)) =
   45.76        let
   45.77          fun arg (s, p) =
   45.78            (if s = "type" then TypArg else Arg)
   45.79 -          (if Lexicon.is_terminal s then SynExt.max_pri else p);
   45.80 +          (if Lexicon.is_terminal s then Syn_Ext.max_pri else p);
   45.81  
   45.82 -        fun xsyms_to_syms (SynExt.Delim s :: xsyms) =
   45.83 +        fun xsyms_to_syms (Syn_Ext.Delim s :: xsyms) =
   45.84                apfst (cons (String s)) (xsyms_to_syms xsyms)
   45.85 -          | xsyms_to_syms (SynExt.Argument s_p :: xsyms) =
   45.86 +          | xsyms_to_syms (Syn_Ext.Argument s_p :: xsyms) =
   45.87                apfst (cons (arg s_p)) (xsyms_to_syms xsyms)
   45.88 -          | xsyms_to_syms (SynExt.Space s :: xsyms) =
   45.89 +          | xsyms_to_syms (Syn_Ext.Space s :: xsyms) =
   45.90                apfst (cons (Space s)) (xsyms_to_syms xsyms)
   45.91 -          | xsyms_to_syms (SynExt.Bg i :: xsyms) =
   45.92 +          | xsyms_to_syms (Syn_Ext.Bg i :: xsyms) =
   45.93                let
   45.94                  val (bsyms, xsyms') = xsyms_to_syms xsyms;
   45.95                  val (syms, xsyms'') = xsyms_to_syms xsyms';
   45.96                in
   45.97                  (Block (i, bsyms) :: syms, xsyms'')
   45.98                end
   45.99 -          | xsyms_to_syms (SynExt.Brk i :: xsyms) =
  45.100 +          | xsyms_to_syms (Syn_Ext.Brk i :: xsyms) =
  45.101                apfst (cons (Break i)) (xsyms_to_syms xsyms)
  45.102 -          | xsyms_to_syms (SynExt.En :: xsyms) = ([], xsyms)
  45.103 +          | xsyms_to_syms (Syn_Ext.En :: xsyms) = ([], xsyms)
  45.104            | xsyms_to_syms [] = ([], []);
  45.105  
  45.106          fun nargs (Arg _ :: syms) = nargs syms + 1
  45.107 @@ -263,7 +263,7 @@
  45.108  fun remove_prtabs mode xprods prtabs =
  45.109    let
  45.110      val tab = mode_tab prtabs mode;
  45.111 -    val fmts = map_filter (fn xprod as SynExt.XProd (_, _, c, _) =>
  45.112 +    val fmts = map_filter (fn xprod as Syn_Ext.XProd (_, _, c, _) =>
  45.113        if null (Symtab.lookup_list tab c) then NONE
  45.114        else xprod_to_fmt xprod) xprods;
  45.115      val tab' = fold (Symtab.remove_list (op =)) fmts tab;
  45.116 @@ -290,15 +290,15 @@
  45.117      fun token_trans a x =
  45.118        (case tokentrf a of
  45.119          NONE =>
  45.120 -          if member (op =) SynExt.standard_token_classes a
  45.121 +          if member (op =) Syn_Ext.standard_token_classes a
  45.122            then SOME (Pretty.str x) else NONE
  45.123        | SOME f => SOME (f ctxt x));
  45.124  
  45.125      (*default applications: prefix / postfix*)
  45.126      val appT =
  45.127 -      if type_mode then TypeExt.tappl_ast_tr'
  45.128 -      else if curried then SynTrans.applC_ast_tr'
  45.129 -      else SynTrans.appl_ast_tr';
  45.130 +      if type_mode then Type_Ext.tappl_ast_tr'
  45.131 +      else if curried then Syn_Trans.applC_ast_tr'
  45.132 +      else Syn_Trans.appl_ast_tr';
  45.133  
  45.134      fun synT _ ([], args) = ([], args)
  45.135        | synT markup (Arg p :: symbs, t :: args) =
  45.136 @@ -333,7 +333,7 @@
  45.137  
  45.138      and parT markup (pr, args, p, p': int) = #1 (synT markup
  45.139            (if p > p' orelse
  45.140 -            (! show_brackets andalso p' <> SynExt.max_pri andalso not (is_chain pr))
  45.141 +            (! show_brackets andalso p' <> Syn_Ext.max_pri andalso not (is_chain pr))
  45.142              then [Block (1, Space "(" :: pr @ [Space ")"])]
  45.143              else pr, args))
  45.144  
    46.1 --- a/src/Pure/Syntax/syn_ext.ML	Mon May 31 19:36:13 2010 +0200
    46.2 +++ b/src/Pure/Syntax/syn_ext.ML	Mon May 31 21:06:57 2010 +0200
    46.3 @@ -41,7 +41,7 @@
    46.4    val chain_pri: int
    46.5    val delims_of: xprod list -> string list list
    46.6    datatype syn_ext =
    46.7 -    SynExt of {
    46.8 +    Syn_Ext of {
    46.9        xprods: xprod list,
   46.10        consts: string list,
   46.11        prmodes: string list,
   46.12 @@ -86,7 +86,7 @@
   46.13    val pure_ext: syn_ext
   46.14  end;
   46.15  
   46.16 -structure SynExt: SYN_EXT =
   46.17 +structure Syn_Ext: SYN_EXT =
   46.18  struct
   46.19  
   46.20  
   46.21 @@ -326,7 +326,7 @@
   46.22  (** datatype syn_ext **)
   46.23  
   46.24  datatype syn_ext =
   46.25 -  SynExt of {
   46.26 +  Syn_Ext of {
   46.27      xprods: xprod list,
   46.28      consts: string list,
   46.29      prmodes: string list,
   46.30 @@ -352,7 +352,7 @@
   46.31      val mfix_consts =
   46.32        distinct (op =) (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
   46.33    in
   46.34 -    SynExt {
   46.35 +    Syn_Ext {
   46.36        xprods = xprods,
   46.37        consts = union (op =) consts mfix_consts,
   46.38        prmodes = distinct (op =) (map (fn (m, _, _) => m) tokentrfuns),
    47.1 --- a/src/Pure/Syntax/syn_trans.ML	Mon May 31 19:36:13 2010 +0200
    47.2 +++ b/src/Pure/Syntax/syn_trans.ML	Mon May 31 21:06:57 2010 +0200
    47.3 @@ -60,7 +60,7 @@
    47.4      (string -> (Proof.context -> term list -> term) option) -> Ast.ast list -> term list
    47.5  end;
    47.6  
    47.7 -structure SynTrans: SYN_TRANS =
    47.8 +structure Syn_Trans: SYN_TRANS =
    47.9  struct
   47.10  
   47.11  
   47.12 @@ -166,7 +166,7 @@
   47.13  
   47.14  (* dddot *)
   47.15  
   47.16 -fun dddot_tr (*"_DDDOT"*) ts = Term.list_comb (Lexicon.var SynExt.dddot_indexname, ts);
   47.17 +fun dddot_tr (*"_DDDOT"*) ts = Term.list_comb (Lexicon.var Syn_Ext.dddot_indexname, ts);
   47.18  
   47.19  
   47.20  (* quote / antiquote *)
   47.21 @@ -354,9 +354,9 @@
   47.22  (* type propositions *)
   47.23  
   47.24  fun type_prop_tr' _ (*"_type_prop"*) T [Const ("\\<^const>Pure.sort_constraint", _)] =
   47.25 -      Lexicon.const "_sort_constraint" $ TypeExt.term_of_typ true T
   47.26 +      Lexicon.const "_sort_constraint" $ Type_Ext.term_of_typ true T
   47.27    | type_prop_tr' show_sorts (*"_type_prop"*) T [t] =
   47.28 -      Lexicon.const "_ofclass" $ TypeExt.term_of_typ show_sorts T $ t
   47.29 +      Lexicon.const "_ofclass" $ Type_Ext.term_of_typ show_sorts T $ t
   47.30    | type_prop_tr' _ (*"_type_prop"*) T ts = raise TYPE ("type_prop_tr'", [T], ts);
   47.31  
   47.32  
   47.33 @@ -394,7 +394,7 @@
   47.34  (* meta implication *)
   47.35  
   47.36  fun impl_ast_tr' (*"==>"*) asts =
   47.37 -  if TypeExt.no_brackets () then raise Match
   47.38 +  if Type_Ext.no_brackets () then raise Match
   47.39    else
   47.40      (case Ast.unfold_ast_p "\\<^const>==>" (Ast.Appl (Ast.Constant "\\<^const>==>" :: asts)) of
   47.41        (prems as _ :: _ :: _, concl) =>
   47.42 @@ -408,14 +408,14 @@
   47.43  (* type reflection *)
   47.44  
   47.45  fun type_tr' show_sorts (*"TYPE"*) (Type ("itself", [T])) ts =
   47.46 -      Term.list_comb (Lexicon.const "_TYPE" $ TypeExt.term_of_typ show_sorts T, ts)
   47.47 +      Term.list_comb (Lexicon.const "_TYPE" $ Type_Ext.term_of_typ show_sorts T, ts)
   47.48    | type_tr' _ _ _ = raise Match;
   47.49  
   47.50  
   47.51  (* type constraints *)
   47.52  
   47.53  fun type_constraint_tr' show_sorts (*"_type_constraint_"*) (Type ("fun", [T, _])) (t :: ts) =
   47.54 -      Term.list_comb (Lexicon.const SynExt.constrainC $ t $ TypeExt.term_of_typ show_sorts T, ts)
   47.55 +      Term.list_comb (Lexicon.const Syn_Ext.constrainC $ t $ Type_Ext.term_of_typ show_sorts T, ts)
   47.56    | type_constraint_tr' _ _ _ = raise Match;
   47.57  
   47.58  
    48.1 --- a/src/Pure/Syntax/syntax.ML	Mon May 31 19:36:13 2010 +0200
    48.2 +++ b/src/Pure/Syntax/syntax.ML	Mon May 31 21:06:57 2010 +0200
    48.3 @@ -168,21 +168,21 @@
    48.4  fun err_dup_trfun name c =
    48.5    error ("More than one " ^ name ^ " for " ^ quote c);
    48.6  
    48.7 -fun remove_trtab trfuns = fold (Symtab.remove SynExt.eq_trfun) trfuns;
    48.8 +fun remove_trtab trfuns = fold (Symtab.remove Syn_Ext.eq_trfun) trfuns;
    48.9  
   48.10  fun update_trtab name trfuns tab = fold Symtab.update_new trfuns (remove_trtab trfuns tab)
   48.11    handle Symtab.DUP c => err_dup_trfun name c;
   48.12  
   48.13 -fun merge_trtabs name tab1 tab2 = Symtab.merge SynExt.eq_trfun (tab1, tab2)
   48.14 +fun merge_trtabs name tab1 tab2 = Symtab.merge Syn_Ext.eq_trfun (tab1, tab2)
   48.15    handle Symtab.DUP c => err_dup_trfun name c;
   48.16  
   48.17  
   48.18  (* print (ast) translations *)
   48.19  
   48.20  fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
   48.21 -fun update_tr'tab trfuns = fold_rev (Symtab.update_list SynExt.eq_trfun) trfuns;
   48.22 -fun remove_tr'tab trfuns = fold (Symtab.remove_list SynExt.eq_trfun) trfuns;
   48.23 -fun merge_tr'tabs tab1 tab2 = Symtab.merge_list SynExt.eq_trfun (tab1, tab2);
   48.24 +fun update_tr'tab trfuns = fold_rev (Symtab.update_list Syn_Ext.eq_trfun) trfuns;
   48.25 +fun remove_tr'tab trfuns = fold (Symtab.remove_list Syn_Ext.eq_trfun) trfuns;
   48.26 +fun merge_tr'tabs tab1 tab2 = Symtab.merge_list Syn_Ext.eq_trfun (tab1, tab2);
   48.27  
   48.28  
   48.29  
   48.30 @@ -239,7 +239,7 @@
   48.31  
   48.32  datatype syntax =
   48.33    Syntax of {
   48.34 -    input: SynExt.xprod list,
   48.35 +    input: Syn_Ext.xprod list,
   48.36      lexicon: Scan.lexicon,
   48.37      gram: Parser.gram,
   48.38      consts: string list,
   48.39 @@ -287,7 +287,7 @@
   48.40      val {input, lexicon, gram, consts = consts1, prmodes = prmodes1,
   48.41        parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab, print_ruletab,
   48.42        print_ast_trtab, tokentrtab, prtabs} = tabs;
   48.43 -    val SynExt.SynExt {xprods, consts = consts2, prmodes = prmodes2,
   48.44 +    val Syn_Ext.Syn_Ext {xprods, consts = consts2, prmodes = prmodes2,
   48.45        parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
   48.46        print_ast_translation, token_translation} = syn_ext;
   48.47      val new_xprods =
   48.48 @@ -296,7 +296,7 @@
   48.49    in
   48.50      Syntax
   48.51      ({input = new_xprods @ input,
   48.52 -      lexicon = fold Scan.extend_lexicon (SynExt.delims_of new_xprods) lexicon,
   48.53 +      lexicon = fold Scan.extend_lexicon (Syn_Ext.delims_of new_xprods) lexicon,
   48.54        gram = Parser.extend_gram gram new_xprods,
   48.55        consts = Library.merge (op =) (consts1, filter_out Lexicon.is_marked consts2),
   48.56        prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
   48.57 @@ -316,7 +316,7 @@
   48.58  
   48.59  fun remove_syntax (mode, inout) syn_ext (Syntax (tabs, _)) =
   48.60    let
   48.61 -    val SynExt.SynExt {xprods, consts = _, prmodes = _,
   48.62 +    val Syn_Ext.Syn_Ext {xprods, consts = _, prmodes = _,
   48.63        parse_ast_translation, parse_rules, parse_translation, print_translation, print_rules,
   48.64        print_ast_translation, token_translation = _} = syn_ext;
   48.65      val {input, lexicon, gram, consts, prmodes,
   48.66 @@ -328,7 +328,7 @@
   48.67    in
   48.68      Syntax
   48.69      ({input = input',
   48.70 -      lexicon = if changed then Scan.make_lexicon (SynExt.delims_of input') else lexicon,
   48.71 +      lexicon = if changed then Scan.make_lexicon (Syn_Ext.delims_of input') else lexicon,
   48.72        gram = if changed then Parser.make_gram input' else gram,
   48.73        consts = consts,
   48.74        prmodes = prmodes,
   48.75 @@ -381,13 +381,13 @@
   48.76  
   48.77  val basic_syntax =
   48.78    empty_syntax
   48.79 -  |> update_syntax mode_default TypeExt.type_ext
   48.80 -  |> update_syntax mode_default SynExt.pure_ext;
   48.81 +  |> update_syntax mode_default Type_Ext.type_ext
   48.82 +  |> update_syntax mode_default Syn_Ext.pure_ext;
   48.83  
   48.84  val basic_nonterms =
   48.85 -  (Lexicon.terminals @ [SynExt.logic, "type", "types", "sort", "classes",
   48.86 -    SynExt.args, SynExt.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
   48.87 -    "asms", SynExt.any, SynExt.sprop, "num_const", "float_const",
   48.88 +  (Lexicon.terminals @ [Syn_Ext.logic, "type", "types", "sort", "classes",
   48.89 +    Syn_Ext.args, Syn_Ext.cargs, "pttrn", "pttrns", "idt", "idts", "aprop",
   48.90 +    "asms", Syn_Ext.any, Syn_Ext.sprop, "num_const", "float_const",
   48.91      "index", "struct"]);
   48.92  
   48.93  
   48.94 @@ -481,13 +481,13 @@
   48.95      val toks = Lexicon.tokenize lexicon xids syms;
   48.96      val _ = List.app Lexicon.report_token toks;
   48.97  
   48.98 -    val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
   48.99 +    val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
  48.100      val pts = Parser.parse gram root' (filter Lexicon.is_proper toks);
  48.101      val len = length pts;
  48.102  
  48.103      val limit = ! ambiguity_limit;
  48.104      fun show_pt pt =
  48.105 -      Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts ctxt (K NONE) [pt])));
  48.106 +      Pretty.string_of (Ast.pretty_ast (hd (Syn_Trans.pts_to_asts ctxt (K NONE) [pt])));
  48.107    in
  48.108      if len <= ! ambiguity_level then ()
  48.109      else if ! ambiguity_is_error then error (ambiguity_msg pos)
  48.110 @@ -497,7 +497,7 @@
  48.111            "\nproduces " ^ string_of_int len ^ " parse trees" ^
  48.112            (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
  48.113            map show_pt (take limit pts))));
  48.114 -    SynTrans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
  48.115 +    Syn_Trans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
  48.116    end;
  48.117  
  48.118  
  48.119 @@ -506,9 +506,9 @@
  48.120  fun read ctxt is_logtype (syn as Syntax (tabs, _)) ty inp =
  48.121    let
  48.122      val {parse_ruletab, parse_trtab, ...} = tabs;
  48.123 -    val asts = read_asts ctxt is_logtype syn false (SynExt.typ_to_nonterm ty) inp;
  48.124 +    val asts = read_asts ctxt is_logtype syn false (Syn_Ext.typ_to_nonterm ty) inp;
  48.125    in
  48.126 -    SynTrans.asts_to_terms ctxt (lookup_tr parse_trtab)
  48.127 +    Syn_Trans.asts_to_terms ctxt (lookup_tr parse_trtab)
  48.128        (map (Ast.normalize_ast (Symtab.lookup_list parse_ruletab)) asts)
  48.129    end;
  48.130  
  48.131 @@ -547,23 +547,23 @@
  48.132  
  48.133  fun standard_parse_term pp check get_sort map_const map_free ctxt is_logtype syn ty (syms, pos) =
  48.134    read ctxt is_logtype syn ty (syms, pos)
  48.135 -  |> map (TypeExt.decode_term get_sort map_const map_free)
  48.136 +  |> map (Type_Ext.decode_term get_sort map_const map_free)
  48.137    |> disambig (Printer.pp_show_brackets pp) check;
  48.138  
  48.139  
  48.140  (* read types *)
  48.141  
  48.142  fun standard_parse_typ ctxt syn get_sort (syms, pos) =
  48.143 -  (case read ctxt (K false) syn SynExt.typeT (syms, pos) of
  48.144 -    [t] => TypeExt.typ_of_term (get_sort (TypeExt.term_sorts t)) t
  48.145 +  (case read ctxt (K false) syn Syn_Ext.typeT (syms, pos) of
  48.146 +    [t] => Type_Ext.typ_of_term (get_sort (Type_Ext.term_sorts t)) t
  48.147    | _ => error (ambiguity_msg pos));
  48.148  
  48.149  
  48.150  (* read sorts *)
  48.151  
  48.152  fun standard_parse_sort ctxt syn (syms, pos) =
  48.153 -  (case read ctxt (K false) syn TypeExt.sortT (syms, pos) of
  48.154 -    [t] => TypeExt.sort_of_term t
  48.155 +  (case read ctxt (K false) syn Type_Ext.sortT (syms, pos) of
  48.156 +    [t] => Type_Ext.sort_of_term t
  48.157    | _ => error (ambiguity_msg pos));
  48.158  
  48.159  
  48.160 @@ -666,9 +666,9 @@
  48.161  
  48.162  fun ext_syntax f decls = update_syntax mode_default (f decls);
  48.163  
  48.164 -val update_trfuns = ext_syntax SynExt.syn_ext_trfuns;
  48.165 -val update_advanced_trfuns = ext_syntax SynExt.syn_ext_advanced_trfuns;
  48.166 -val extend_tokentrfuns = ext_syntax SynExt.syn_ext_tokentrfuns;
  48.167 +val update_trfuns = ext_syntax Syn_Ext.syn_ext_trfuns;
  48.168 +val update_advanced_trfuns = ext_syntax Syn_Ext.syn_ext_advanced_trfuns;
  48.169 +val extend_tokentrfuns = ext_syntax Syn_Ext.syn_ext_tokentrfuns;
  48.170  
  48.171  fun update_type_gram add prmode decls =
  48.172    (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_types decls);
  48.173 @@ -677,13 +677,13 @@
  48.174    (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts is_logtype decls);
  48.175  
  48.176  fun update_trrules ctxt is_logtype syn =
  48.177 -  ext_syntax SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
  48.178 +  ext_syntax Syn_Ext.syn_ext_rules o read_rules ctxt is_logtype syn;
  48.179  
  48.180  fun remove_trrules ctxt is_logtype syn =
  48.181 -  remove_syntax mode_default o SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
  48.182 +  remove_syntax mode_default o Syn_Ext.syn_ext_rules o read_rules ctxt is_logtype syn;
  48.183  
  48.184 -val update_trrules_i = ext_syntax SynExt.syn_ext_rules o cert_rules;
  48.185 -val remove_trrules_i = remove_syntax mode_default o SynExt.syn_ext_rules o cert_rules;
  48.186 +val update_trrules_i = ext_syntax Syn_Ext.syn_ext_rules o cert_rules;
  48.187 +val remove_trrules_i = remove_syntax mode_default o Syn_Ext.syn_ext_rules o cert_rules;
  48.188  
  48.189  
  48.190  
  48.191 @@ -798,7 +798,7 @@
  48.192  
  48.193  val check_typs = gen_check fst false;
  48.194  val check_terms = gen_check snd false;
  48.195 -fun check_props ctxt = map (TypeExt.type_constraint propT) #> check_terms ctxt;
  48.196 +fun check_props ctxt = map (Type_Ext.type_constraint propT) #> check_terms ctxt;
  48.197  
  48.198  val check_typ = singleton o check_typs;
  48.199  val check_term = singleton o check_terms;
  48.200 @@ -905,7 +905,7 @@
  48.201  
  48.202  
  48.203  (*export parts of internal Syntax structures*)
  48.204 -open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
  48.205 +open Lexicon Syn_Ext Ast Parser Type_Ext Syn_Trans Mixfix Printer;
  48.206  
  48.207  end;
  48.208  
  48.209 @@ -913,9 +913,9 @@
  48.210  open Basic_Syntax;
  48.211  
  48.212  forget_structure "Ast";
  48.213 -forget_structure "SynExt";
  48.214 +forget_structure "Syn_Ext";
  48.215  forget_structure "Parser";
  48.216 -forget_structure "TypeExt";
  48.217 -forget_structure "SynTrans";
  48.218 +forget_structure "Type_Ext";
  48.219 +forget_structure "Syn_Trans";
  48.220  forget_structure "Mixfix";
  48.221  forget_structure "Printer";
    49.1 --- a/src/Pure/Syntax/type_ext.ML	Mon May 31 19:36:13 2010 +0200
    49.2 +++ b/src/Pure/Syntax/type_ext.ML	Mon May 31 21:06:57 2010 +0200
    49.3 @@ -27,10 +27,10 @@
    49.4    val term_of_sort: sort -> term
    49.5    val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    49.6    val sortT: typ
    49.7 -  val type_ext: SynExt.syn_ext
    49.8 +  val type_ext: Syn_Ext.syn_ext
    49.9  end;
   49.10  
   49.11 -structure TypeExt: TYPE_EXT =
   49.12 +structure Type_Ext: TYPE_EXT =
   49.13  struct
   49.14  
   49.15  (** input utils **)
   49.16 @@ -242,7 +242,7 @@
   49.17  val classesT = Type ("classes", []);
   49.18  val typesT = Type ("types", []);
   49.19  
   49.20 -local open Lexicon SynExt in
   49.21 +local open Lexicon Syn_Ext in
   49.22  
   49.23  val type_ext = syn_ext' false (K false)
   49.24    [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
   49.25 @@ -271,7 +271,7 @@
   49.26     Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
   49.27     Mfix ("'_",          typeT,                         "\\<^type>dummy", [], max_pri)]
   49.28    ["_type_prop"]
   49.29 -  ([], [], [], map SynExt.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
   49.30 +  ([], [], [], map Syn_Ext.mk_trfun [("\\<^type>fun", K fun_ast_tr')])
   49.31    []
   49.32    ([], []);
   49.33  
    50.1 --- a/src/Pure/System/isabelle_process.ML	Mon May 31 19:36:13 2010 +0200
    50.2 +++ b/src/Pure/System/isabelle_process.ML	Mon May 31 21:06:57 2010 +0200
    50.3 @@ -67,9 +67,9 @@
    50.4      val path = File.platform_path (Path.explode out);
    50.5      val out_stream = TextIO.openOut path;  (*fifo blocks until reader is ready*)
    50.6      val _ = OS.FileSys.remove path;  (*prevent alien access, indicate writer is ready*)
    50.7 -    val _ = SimpleThread.fork false (auto_flush out_stream);
    50.8 -    val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
    50.9 -    val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
   50.10 +    val _ = Simple_Thread.fork false (auto_flush out_stream);
   50.11 +    val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
   50.12 +    val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
   50.13    in
   50.14      Output.status_fn   := standard_message out_stream "B";
   50.15      Output.writeln_fn  := standard_message out_stream "C";
    51.1 --- a/src/Pure/System/isar.ML	Mon May 31 19:36:13 2010 +0200
    51.2 +++ b/src/Pure/System/isar.ML	Mon May 31 21:06:57 2010 +0200
    51.3 @@ -72,7 +72,7 @@
    51.4  
    51.5  fun find_and_undo _ [] = error "Undo history exhausted"
    51.6    | find_and_undo which ((prev, tr) :: hist) =
    51.7 -      ((case Toplevel.init_of tr of SOME name => ThyInfo.kill_thy name | NONE => ());
    51.8 +      ((case Toplevel.init_of tr of SOME name => Thy_Info.kill_thy name | NONE => ());
    51.9          if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist);
   51.10  
   51.11  in
    52.1 --- a/src/Pure/System/session.ML	Mon May 31 19:36:13 2010 +0200
    52.2 +++ b/src/Pure/System/session.ML	Mon May 31 21:06:57 2010 +0200
    52.3 @@ -73,7 +73,7 @@
    52.4  (* finish *)
    52.5  
    52.6  fun finish () =
    52.7 -  (ThyInfo.finish ();
    52.8 +  (Thy_Info.finish ();
    52.9      Present.finish ();
   52.10      Future.shutdown ();
   52.11      session_finished := true);
   52.12 @@ -97,7 +97,7 @@
   52.13    ((fn () =>
   52.14       (init reset parent name;
   52.15        Present.init build info doc doc_graph doc_versions (path ()) name
   52.16 -        (dumping dump) (get_rpath rpath) verbose (map ThyInfo.get_theory (ThyInfo.get_names ()));
   52.17 +        (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
   52.18        if timing then
   52.19          let
   52.20            val start = start_timing ();
    53.1 --- a/src/Pure/Thy/present.ML	Mon May 31 19:36:13 2010 +0200
    53.2 +++ b/src/Pure/Thy/present.ML	Mon May 31 21:06:57 2010 +0200
    53.3 @@ -461,7 +461,7 @@
    53.4      val parent_specs = map (parent_link remote_path path) parents;
    53.5  
    53.6      fun prep_file (raw_path, loadit) =
    53.7 -      (case ThyLoad.check_ml dir raw_path of
    53.8 +      (case Thy_Load.check_ml dir raw_path of
    53.9          SOME (path, _) =>
   53.10            let
   53.11              val base = Path.base path;
    54.1 --- a/src/Pure/Thy/thm_deps.ML	Mon May 31 19:36:13 2010 +0200
    54.2 +++ b/src/Pure/Thy/thm_deps.ML	Mon May 31 21:06:57 2010 +0200
    54.3 @@ -24,7 +24,7 @@
    54.4              val session =
    54.5                (case prefix of
    54.6                  a :: _ =>
    54.7 -                  (case ThyInfo.lookup_theory a of
    54.8 +                  (case Thy_Info.lookup_theory a of
    54.9                      SOME thy =>
   54.10                        (case Present.session_name thy of
   54.11                          "" => []
    55.1 --- a/src/Pure/Thy/thy_info.ML	Mon May 31 19:36:13 2010 +0200
    55.2 +++ b/src/Pure/Thy/thy_info.ML	Mon May 31 21:06:57 2010 +0200
    55.3 @@ -41,7 +41,7 @@
    55.4    val finish: unit -> unit
    55.5  end;
    55.6  
    55.7 -structure ThyInfo: THY_INFO =
    55.8 +structure Thy_Info: THY_INFO =
    55.9  struct
   55.10  
   55.11  (** theory loader actions and hooks **)
   55.12 @@ -292,12 +292,12 @@
   55.13  
   55.14  fun run_file path =
   55.15    (case Option.map (Context.theory_name o Context.the_theory) (Context.thread_data ()) of
   55.16 -    NONE => (ThyLoad.load_ml Path.current path; ())
   55.17 +    NONE => (Thy_Load.load_ml Path.current path; ())
   55.18    | SOME name =>
   55.19        (case lookup_deps name of
   55.20          SOME deps =>
   55.21 -          change_deps name (provide path name (ThyLoad.load_ml (master_dir' deps) path))
   55.22 -      | NONE => (ThyLoad.load_ml Path.current path; ())));
   55.23 +          change_deps name (provide path name (Thy_Load.load_ml (master_dir' deps) path))
   55.24 +      | NONE => (Thy_Load.load_ml Path.current path; ())));
   55.25  
   55.26  in
   55.27  
   55.28 @@ -306,7 +306,7 @@
   55.29      val dir = master_directory name;
   55.30      val _ = check_unfinished error name;
   55.31    in
   55.32 -    (case ThyLoad.check_file dir path of
   55.33 +    (case Thy_Load.check_file dir path of
   55.34        SOME path_info => change_deps name (provide path name path_info)
   55.35      | NONE => error ("Could not find file " ^ quote (Path.implode path)))
   55.36    end;
   55.37 @@ -429,7 +429,7 @@
   55.38    let val info' =
   55.39      (case info of NONE => NONE
   55.40      | SOME (_, id) =>
   55.41 -        (case ThyLoad.check_ml (master_dir master) src_path of NONE => NONE
   55.42 +        (case Thy_Load.check_ml (master_dir master) src_path of NONE => NONE
   55.43          | SOME (path', id') => if id <> id' then NONE else SOME (path', id')))
   55.44    in (src_path, info') end;
   55.45  
   55.46 @@ -437,16 +437,16 @@
   55.47    (case lookup_deps name of
   55.48      SOME NONE => (true, NONE, get_parents name)
   55.49    | NONE =>
   55.50 -      let val {master, text, imports = parents, uses = files} = ThyLoad.deps_thy dir name
   55.51 +      let val {master, text, imports = parents, uses = files} = Thy_Load.deps_thy dir name
   55.52        in (false, init_deps (SOME master) text parents files, parents) end
   55.53    | SOME (SOME {update_time, master, text, parents, files}) =>
   55.54        let
   55.55 -        val (thy_path, thy_id) = ThyLoad.check_thy dir name;
   55.56 +        val (thy_path, thy_id) = Thy_Load.check_thy dir name;
   55.57          val master' = SOME (thy_path, thy_id);
   55.58        in
   55.59          if Option.map #2 master <> SOME thy_id then
   55.60            let val {text = text', imports = parents', uses = files', ...} =
   55.61 -            ThyLoad.deps_thy dir name;
   55.62 +            Thy_Load.deps_thy dir name;
   55.63            in (false, init_deps master' text' parents' files', parents') end
   55.64          else
   55.65            let
   55.66 @@ -571,7 +571,7 @@
   55.67      val _ = map get_theory (get_parents name);
   55.68      val _ = check_unfinished error name;
   55.69      val _ = touch_thy name;
   55.70 -    val master = #master (ThyLoad.deps_thy Path.current name);
   55.71 +    val master = #master (Thy_Load.deps_thy Path.current name);
   55.72      val upd_time = #2 (Management_Data.get thy);
   55.73    in
   55.74      CRITICAL (fn () =>
    56.1 --- a/src/Pure/Thy/thy_load.ML	Mon May 31 19:36:13 2010 +0200
    56.2 +++ b/src/Pure/Thy/thy_load.ML	Mon May 31 21:06:57 2010 +0200
    56.3 @@ -31,10 +31,9 @@
    56.4    val load_ml: Path.T -> Path.T -> Path.T * File.ident
    56.5  end;
    56.6  
    56.7 -structure ThyLoad: THY_LOAD =
    56.8 +structure Thy_Load: THY_LOAD =
    56.9  struct
   56.10  
   56.11 -
   56.12  (* maintain load path *)
   56.13  
   56.14  local val load_path = Unsynchronized.ref [Path.current] in
   56.15 @@ -132,5 +131,5 @@
   56.16  
   56.17  end;
   56.18  
   56.19 -structure Basic_Thy_Load: BASIC_THY_LOAD = ThyLoad;
   56.20 +structure Basic_Thy_Load: BASIC_THY_LOAD = Thy_Load;
   56.21  open Basic_Thy_Load;
    57.1 --- a/src/Pure/Thy/thy_output.ML	Mon May 31 19:36:13 2010 +0200
    57.2 +++ b/src/Pure/Thy/thy_output.ML	Mon May 31 21:06:57 2010 +0200
    57.3 @@ -33,7 +33,7 @@
    57.4    val output: Pretty.T list -> string
    57.5  end;
    57.6  
    57.7 -structure ThyOutput: THY_OUTPUT =
    57.8 +structure Thy_Output: THY_OUTPUT =
    57.9  struct
   57.10  
   57.11  (** global options **)
    58.1 --- a/src/Pure/Thy/thy_syntax.ML	Mon May 31 19:36:13 2010 +0200
    58.2 +++ b/src/Pure/Thy/thy_syntax.ML	Mon May 31 21:06:57 2010 +0200
    58.3 @@ -25,7 +25,7 @@
    58.4      (span * span list * bool, (span, 'a) Source.source) Source.source
    58.5  end;
    58.6  
    58.7 -structure ThySyntax: THY_SYNTAX =
    58.8 +structure Thy_Syntax: THY_SYNTAX =
    58.9  struct
   58.10  
   58.11  (** tokens **)
    59.1 --- a/src/Pure/context.ML	Mon May 31 19:36:13 2010 +0200
    59.2 +++ b/src/Pure/context.ML	Mon May 31 21:06:57 2010 +0200
    59.3 @@ -325,7 +325,7 @@
    59.4  local
    59.5    val lock = Mutex.mutex ();
    59.6  in
    59.7 -  fun SYNCHRONIZED e = SimpleThread.synchronized "theory" lock e;
    59.8 +  fun SYNCHRONIZED e = Simple_Thread.synchronized "theory" lock e;
    59.9  end;
   59.10  
   59.11  fun create_thy self draft ids data ancestry history =
    60.1 --- a/src/Pure/morphism.ML	Mon May 31 19:36:13 2010 +0200
    60.2 +++ b/src/Pure/morphism.ML	Mon May 31 21:06:57 2010 +0200
    60.3 @@ -79,5 +79,5 @@
    60.4  
    60.5  end;
    60.6  
    60.7 -structure BasicMorphism: BASIC_MORPHISM = Morphism;
    60.8 -open BasicMorphism;
    60.9 +structure Basic_Morphism: BASIC_MORPHISM = Morphism;
   60.10 +open Basic_Morphism;
    61.1 --- a/src/Pure/proofterm.ML	Mon May 31 19:36:13 2010 +0200
    61.2 +++ b/src/Pure/proofterm.ML	Mon May 31 21:06:57 2010 +0200
    61.3 @@ -1328,7 +1328,7 @@
    61.4  
    61.5  (**** theory data ****)
    61.6  
    61.7 -structure ProofData = Theory_Data
    61.8 +structure Data = Theory_Data
    61.9  (
   61.10    type T =
   61.11      (stamp * (proof * proof)) list *
   61.12 @@ -1341,11 +1341,11 @@
   61.13        AList.merge (op =) (K true) (procs1, procs2));
   61.14  );
   61.15  
   61.16 -fun get_data thy = let val (rules, procs) = ProofData.get thy in (map #2 rules, map #2 procs) end;
   61.17 +fun get_data thy = let val (rules, procs) = Data.get thy in (map #2 rules, map #2 procs) end;
   61.18  fun rew_proof thy = rewrite_prf fst (get_data thy);
   61.19  
   61.20 -fun add_prf_rrule r = (ProofData.map o apfst) (cons (stamp (), r));
   61.21 -fun add_prf_rproc p = (ProofData.map o apsnd) (cons (stamp (), p));
   61.22 +fun add_prf_rrule r = (Data.map o apfst) (cons (stamp (), r));
   61.23 +fun add_prf_rproc p = (Data.map o apsnd) (cons (stamp (), p));
   61.24  
   61.25  
   61.26  (***** promises *****)
    62.1 --- a/src/Pure/pure_setup.ML	Mon May 31 19:36:13 2010 +0200
    62.2 +++ b/src/Pure/pure_setup.ML	Mon May 31 21:06:57 2010 +0200
    62.3 @@ -6,14 +6,14 @@
    62.4  
    62.5  (* the Pure theories *)
    62.6  
    62.7 -val theory = ThyInfo.get_theory;
    62.8 +val theory = Thy_Info.get_theory;
    62.9  
   62.10  Context.>> (Context.map_theory
   62.11   (Outer_Syntax.process_file (Path.explode "Pure.thy") #>
   62.12    Theory.end_theory));
   62.13  structure Pure = struct val thy = ML_Context.the_global_context () end;
   62.14  Context.set_thread_data NONE;
   62.15 -ThyInfo.register_theory Pure.thy;
   62.16 +Thy_Info.register_theory Pure.thy;
   62.17  
   62.18  
   62.19  (* ML toplevel pretty printing *)
   62.20 @@ -47,11 +47,11 @@
   62.21  
   62.22  (* ML toplevel use commands *)
   62.23  
   62.24 -fun use name = Toplevel.program (fn () => ThyInfo.use name);
   62.25 -fun use_thys name = Toplevel.program (fn () => ThyInfo.use_thys name);
   62.26 -fun use_thy name = Toplevel.program (fn () => ThyInfo.use_thy name);
   62.27 -fun time_use name = Toplevel.program (fn () => ThyInfo.time_use name);
   62.28 -fun time_use_thy name = Toplevel.program (fn () => ThyInfo.time_use_thy name);
   62.29 +fun use name = Toplevel.program (fn () => Thy_Info.use name);
   62.30 +fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
   62.31 +fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
   62.32 +fun time_use name = Toplevel.program (fn () => Thy_Info.time_use name);
   62.33 +fun time_use_thy name = Toplevel.program (fn () => Thy_Info.time_use_thy name);
   62.34  
   62.35  
   62.36  (* misc *)
    63.1 --- a/src/Pure/pure_thy.ML	Mon May 31 19:36:13 2010 +0200
    63.2 +++ b/src/Pure/pure_thy.ML	Mon May 31 21:06:57 2010 +0200
    63.3 @@ -52,7 +52,7 @@
    63.4  
    63.5  (** theory data **)
    63.6  
    63.7 -structure FactsData = Theory_Data
    63.8 +structure Global_Facts = Theory_Data
    63.9  (
   63.10    type T = Facts.T * thm list;
   63.11    val empty = (Facts.empty, []);
   63.12 @@ -63,19 +63,19 @@
   63.13  
   63.14  (* facts *)
   63.15  
   63.16 -val facts_of = #1 o FactsData.get;
   63.17 +val facts_of = #1 o Global_Facts.get;
   63.18  
   63.19  val intern_fact = Facts.intern o facts_of;
   63.20  val defined_fact = Facts.defined o facts_of;
   63.21  
   63.22 -fun hide_fact fully name = FactsData.map (apfst (Facts.hide fully name));
   63.23 +fun hide_fact fully name = Global_Facts.map (apfst (Facts.hide fully name));
   63.24  
   63.25  
   63.26  (* proofs *)
   63.27  
   63.28 -fun register_proofs (thy, thms) = (FactsData.map (apsnd (append thms)) thy, thms);
   63.29 +fun register_proofs (thy, thms) = (Global_Facts.map (apsnd (append thms)) thy, thms);
   63.30  
   63.31 -fun join_proofs thy = Thm.join_proofs (rev (#2 (FactsData.get thy)));
   63.32 +fun join_proofs thy = Thm.join_proofs (rev (#2 (Global_Facts.get thy)));
   63.33  
   63.34  
   63.35  
   63.36 @@ -143,7 +143,7 @@
   63.37        val (thy', thms') =
   63.38          register_proofs (apsnd (post_name name) (app_att (thy, pre_name name thms)));
   63.39        val thms'' = map (Thm.transfer thy') thms';
   63.40 -      val thy'' = thy' |> (FactsData.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
   63.41 +      val thy'' = thy' |> (Global_Facts.map o apfst) (Facts.add_global naming (b, thms'') #> snd);
   63.42      in (thms'', thy'') end;
   63.43  
   63.44  
   63.45 @@ -178,7 +178,7 @@
   63.46  (* add_thms_dynamic *)
   63.47  
   63.48  fun add_thms_dynamic (b, f) thy = thy
   63.49 -  |> (FactsData.map o apfst)
   63.50 +  |> (Global_Facts.map o apfst)
   63.51        (Facts.add_dynamic (Sign.naming_of thy) (b, f) #> snd);
   63.52  
   63.53  
   63.54 @@ -252,7 +252,7 @@
   63.55    ("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)),
   63.56    ("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))];
   63.57  
   63.58 -structure OldApplSyntax = Theory_Data
   63.59 +structure Old_Appl_Syntax = Theory_Data
   63.60  (
   63.61    type T = bool;
   63.62    val empty = false;
   63.63 @@ -262,10 +262,10 @@
   63.64      else error "Cannot merge theories with different application syntax";
   63.65  );
   63.66  
   63.67 -val old_appl_syntax = OldApplSyntax.get;
   63.68 +val old_appl_syntax = Old_Appl_Syntax.get;
   63.69  
   63.70  val old_appl_syntax_setup =
   63.71 -  OldApplSyntax.put true #>
   63.72 +  Old_Appl_Syntax.put true #>
   63.73    Sign.del_modesyntax_i Syntax.mode_default applC_syntax #>
   63.74    Sign.add_syntax_i appl_syntax;
   63.75  
   63.76 @@ -274,7 +274,7 @@
   63.77  
   63.78  val _ = Context.>> (Context.map_theory
   63.79    (Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
   63.80 -   OldApplSyntax.put false #>
   63.81 +   Old_Appl_Syntax.put false #>
   63.82     Sign.add_types
   63.83     [(Binding.name "fun", 2, NoSyn),
   63.84      (Binding.name "prop", 0, NoSyn),
    64.1 --- a/src/Pure/simplifier.ML	Mon May 31 19:36:13 2010 +0200
    64.2 +++ b/src/Pure/simplifier.ML	Mon May 31 21:06:57 2010 +0200
    64.3 @@ -100,7 +100,7 @@
    64.4  
    64.5  (** simpset data **)
    64.6  
    64.7 -structure SimpsetData = Generic_Data
    64.8 +structure Simpset = Generic_Data
    64.9  (
   64.10    type T = simpset;
   64.11    val empty = empty_ss;
   64.12 @@ -108,8 +108,8 @@
   64.13    val merge = merge_ss;
   64.14  );
   64.15  
   64.16 -val get_ss = SimpsetData.get;
   64.17 -fun map_ss f context = SimpsetData.map (with_context (Context.proof_of context) f) context;
   64.18 +val get_ss = Simpset.get;
   64.19 +fun map_ss f context = Simpset.map (with_context (Context.proof_of context) f) context;
   64.20  
   64.21  
   64.22  (* attributes *)
    65.1 --- a/src/Tools/Code/code_eval.ML	Mon May 31 19:36:13 2010 +0200
    65.2 +++ b/src/Tools/Code/code_eval.ML	Mon May 31 21:06:57 2010 +0200
    65.3 @@ -173,7 +173,7 @@
    65.4        end
    65.5    | process (code_body, _) _ (SOME file_name) thy =
    65.6        let
    65.7 -        val preamble = "(* Generated from " ^ Path.implode (ThyLoad.thy_path (Context.theory_name thy))
    65.8 +        val preamble = "(* Generated from " ^ Path.implode (Thy_Load.thy_path (Context.theory_name thy))
    65.9            ^ "; DO NOT EDIT! *)";
   65.10          val _ = File.write (Path.explode file_name) (preamble ^ "\n\n" ^ code_body);
   65.11        in
    66.1 --- a/src/Tools/Code/code_thingol.ML	Mon May 31 19:36:13 2010 +0200
    66.2 +++ b/src/Tools/Code/code_thingol.ML	Mon May 31 21:06:57 2010 +0200
    66.3 @@ -882,7 +882,7 @@
    66.4      fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy');
    66.5      fun read_const_expr "*" = ([], consts_of thy)
    66.6        | read_const_expr s = if String.isSuffix ".*" s
    66.7 -          then ([], consts_of_select (ThyInfo.the_theory (unsuffix ".*" s) thy))
    66.8 +          then ([], consts_of_select (Thy_Info.the_theory (unsuffix ".*" s) thy))
    66.9            else ([Code.read_const thy s], []);
   66.10    in pairself flat o split_list o map read_const_expr end;
   66.11  
    67.1 --- a/src/Tools/WWW_Find/find_theorems.ML	Mon May 31 19:36:13 2010 +0200
    67.2 +++ b/src/Tools/WWW_Find/find_theorems.ML	Mon May 31 21:06:57 2010 +0200
    67.3 @@ -5,8 +5,9 @@
    67.4  *)
    67.5  
    67.6  local
    67.7 +
    67.8  val default_limit = 20;
    67.9 -val thy_names = sort string_ord (ThyInfo.get_names ());
   67.10 +val thy_names = sort string_ord (Thy_Info.get_names ());
   67.11  
   67.12  val find_theorems_url = "find_theorems";
   67.13  
   67.14 @@ -234,7 +235,9 @@
   67.15      Xhtml.write_close send header
   67.16    end;
   67.17  in
   67.18 +
   67.19  val () = show_question_marks := false;
   67.20  val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems);
   67.21 +
   67.22  end;
   67.23