# HG changeset patch
# User wenzelm
# Date 1216111779 -7200
# Node ID beb9b5f07dbc4916c1e86045247d00acb4ea337d
# Parent  bc47d30747e615650271ead76543ca7caee9461a
adapted ThyInfo.end_theory;

diff -r bc47d30747e6 -r beb9b5f07dbc doc-src/IsarImplementation/Thy/document/integration.tex
--- a/doc-src/IsarImplementation/Thy/document/integration.tex	Tue Jul 15 09:30:39 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/document/integration.tex	Tue Jul 15 10:49:39 2008 +0200
@@ -441,7 +441,7 @@
   \indexml{ThyInfo.touch\_thy}\verb|ThyInfo.touch_thy: string -> unit| \\
   \indexml{ThyInfo.remove\_thy}\verb|ThyInfo.remove_thy: string -> unit| \\[1ex]
   \indexml{ThyInfo.begin\_theory}\verb|ThyInfo.begin_theory|\verb|: ... -> bool -> theory| \\
-  \indexml{ThyInfo.end\_theory}\verb|ThyInfo.end_theory: theory -> theory| \\
+  \indexml{ThyInfo.end\_theory}\verb|ThyInfo.end_theory: theory -> unit| \\
   \indexml{ThyInfo.register\_theory}\verb|ThyInfo.register_theory: theory -> unit| \\[1ex]
   \verb|datatype action = Update |\verb,|,\verb| Outdate |\verb,|,\verb| Remove| \\
   \indexml{ThyInfo.add\_hook}\verb|ThyInfo.add_hook: (ThyInfo.action -> string -> unit) -> unit| \\
@@ -473,8 +473,7 @@
   normally not invoked directly.
 
   \item \verb|ThyInfo.end_theory| concludes the loading of a theory
-  proper.  An attached theory {\ML} file may be still loaded later on.
-  This is function is normally not invoked directly.
+  proper and stores the result in the theory database.
 
   \item \verb|ThyInfo.register_theory|~\isa{text\ thy} registers an
   existing theory value with the theory loader database.  There is no
diff -r bc47d30747e6 -r beb9b5f07dbc doc-src/IsarImplementation/Thy/integration.thy
--- a/doc-src/IsarImplementation/Thy/integration.thy	Tue Jul 15 09:30:39 2008 +0200
+++ b/doc-src/IsarImplementation/Thy/integration.thy	Tue Jul 15 10:49:39 2008 +0200
@@ -371,7 +371,7 @@
   @{index_ML ThyInfo.touch_thy: "string -> unit"} \\
   @{index_ML ThyInfo.remove_thy: "string -> unit"} \\[1ex]
   @{index_ML ThyInfo.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
-  @{index_ML ThyInfo.end_theory: "theory -> theory"} \\
+  @{index_ML ThyInfo.end_theory: "theory -> unit"} \\
   @{index_ML ThyInfo.register_theory: "theory -> unit"} \\[1ex]
   @{verbatim "datatype action = Update | Outdate | Remove"} \\
   @{index_ML ThyInfo.add_hook: "(ThyInfo.action -> string -> unit) -> unit"} \\
@@ -403,8 +403,7 @@
   normally not invoked directly.
 
   \item @{ML ThyInfo.end_theory} concludes the loading of a theory
-  proper.  An attached theory {\ML} file may be still loaded later on.
-  This is function is normally not invoked directly.
+  proper and stores the result in the theory database.
 
   \item @{ML ThyInfo.register_theory}~@{text "text thy"} registers an
   existing theory value with the theory loader database.  There is no