1.1 --- a/doc-src/IsarImplementation/Thy/Integration.thy	Mon May 31 19:36:13 2010 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/Integration.thy	Mon May 31 21:06:57 2010 +0200
     1.3 @@ -368,13 +368,13 @@
     1.4    @{index_ML theory: "string -> theory"} \\
     1.5    @{index_ML use_thy: "string -> unit"} \\
     1.6    @{index_ML use_thys: "string list -> unit"} \\
     1.7 -  @{index_ML ThyInfo.touch_thy: "string -> unit"} \\
     1.8 -  @{index_ML ThyInfo.remove_thy: "string -> unit"} \\[1ex]
     1.9 -  @{index_ML ThyInfo.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
    1.10 -  @{index_ML ThyInfo.end_theory: "theory -> unit"} \\
    1.11 -  @{index_ML ThyInfo.register_theory: "theory -> unit"} \\[1ex]
    1.12 +  @{index_ML Thy_Info.touch_thy: "string -> unit"} \\
    1.13 +  @{index_ML Thy_Info.remove_thy: "string -> unit"} \\[1ex]
    1.14 +  @{index_ML Thy_Info.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
    1.15 +  @{index_ML Thy_Info.end_theory: "theory -> unit"} \\
    1.16 +  @{index_ML Thy_Info.register_theory: "theory -> unit"} \\[1ex]
    1.17    @{verbatim "datatype action = Update | Outdate | Remove"} \\
    1.18 -  @{index_ML ThyInfo.add_hook: "(ThyInfo.action -> string -> unit) -> unit"} \\
    1.19 +  @{index_ML Thy_Info.add_hook: "(Thy_Info.action -> string -> unit) -> unit"} \\
    1.20    \end{mldecls}
    1.21  
    1.22    \begin{description}
    1.23 @@ -395,24 +395,24 @@
    1.24    intrinsic parallelism can be exploited by the system, to speedup
    1.25    loading.
    1.26  
    1.27 -  \item @{ML ThyInfo.touch_thy}~@{text A} performs and @{text outdate} action
    1.28 +  \item @{ML Thy_Info.touch_thy}~@{text A} performs and @{text outdate} action
    1.29    on theory @{text A} and all descendants.
    1.30  
    1.31 -  \item @{ML ThyInfo.remove_thy}~@{text A} deletes theory @{text A} and all
    1.32 +  \item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all
    1.33    descendants from the theory database.
    1.34  
    1.35 -  \item @{ML ThyInfo.begin_theory} is the basic operation behind a
    1.36 +  \item @{ML Thy_Info.begin_theory} is the basic operation behind a
    1.37    @{text \<THEORY>} header declaration.  This {\ML} function is
    1.38    normally not invoked directly.
    1.39  
    1.40 -  \item @{ML ThyInfo.end_theory} concludes the loading of a theory
    1.41 +  \item @{ML Thy_Info.end_theory} concludes the loading of a theory
    1.42    proper and stores the result in the theory database.
    1.43  
    1.44 -  \item @{ML ThyInfo.register_theory}~@{text "text thy"} registers an
    1.45 +  \item @{ML Thy_Info.register_theory}~@{text "text thy"} registers an
    1.46    existing theory value with the theory loader database.  There is no
    1.47    management of associated sources.
    1.48  
    1.49 -  \item @{ML "ThyInfo.add_hook"}~@{text f} registers function @{text
    1.50 +  \item @{ML "Thy_Info.add_hook"}~@{text f} registers function @{text
    1.51    f} as a hook for theory database actions.  The function will be
    1.52    invoked with the action and theory name being involved; thus derived
    1.53    actions may be performed in associated system components, e.g.\