1.1 --- a/doc-src/IsarImplementation/Thy/ML.thy	Thu Oct 14 21:55:21 2010 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/ML.thy	Fri Oct 15 19:19:41 2010 +0100
     1.3 @@ -145,6 +145,8 @@
     1.4    \begin{mldecls}
     1.5    @{index_ML ML_Context.the_generic_context: "unit -> Context.generic"} \\
     1.6    @{index_ML "Context.>> ": "(Context.generic -> Context.generic) -> unit"} \\
     1.7 +  @{index_ML bind_thms: "string * thm list -> unit"} \\
     1.8 +  @{index_ML bind_thm: "string * thm -> unit"} \\
     1.9    \end{mldecls}
    1.10  
    1.11    \begin{description}
    1.12 @@ -158,6 +160,14 @@
    1.13    \item @{ML "Context.>>"}~@{text f} applies context transformation
    1.14    @{text f} to the implicit context of the ML toplevel.
    1.15  
    1.16 +  \item @{ML bind_thms}~@{text "(name, thms)"} stores a list of
    1.17 +  theorems produced in ML both in the (global) theory context and the
    1.18 +  ML toplevel, associating it with the provided name.  Theorems are
    1.19 +  put into a global ``standard'' format before being stored.
    1.20 +
    1.21 +  \item @{ML bind_thm} is similar to @{ML bind_thms} but refers to a
    1.22 +  singleton theorem.
    1.23 +
    1.24    \end{description}
    1.25  
    1.26    It is very important to note that the above functions are really

     2.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Thu Oct 14 21:55:21 2010 +0100
     2.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Fri Oct 15 19:19:41 2010 +0100
     2.3 @@ -837,11 +837,6 @@
     2.4      @{command_def "attribute_setup"} & : & @{text "theory \<rightarrow> theory"} \\
     2.5    \end{matharray}
     2.6  
     2.7 -  \begin{mldecls}
     2.8 -    @{index_ML bind_thms: "string * thm list -> unit"} \\
     2.9 -    @{index_ML bind_thm: "string * thm -> unit"} \\
    2.10 -  \end{mldecls}
    2.11 -
    2.12    \begin{rail}
    2.13      'use' name
    2.14      ;
    2.15 @@ -918,20 +913,6 @@
    2.16            let val context' = context
    2.17            in context' end)) *}  "my declaration"
    2.18  
    2.19 -text {*
    2.20 -  \begin{description}
    2.21 -
    2.22 -  \item @{ML bind_thms}~@{text "(name, thms)"} stores a list of
    2.23 -  theorems produced in ML both in the theory context and the ML
    2.24 -  toplevel, associating it with the provided name.  Theorems are put
    2.25 -  into a global ``standard'' format before being stored.
    2.26 -
    2.27 -  \item @{ML bind_thm} is similar to @{ML bind_thms} but refers to a
    2.28 -  singleton theorem.
    2.29 -  
    2.30 -  \end{description}
    2.31 -*}
    2.32 -
    2.33  
    2.34  section {* Primitive specification elements *}
    2.35  

     3.1 --- a/doc-src/IsarRef/Thy/document/Spec.tex	Thu Oct 14 21:55:21 2010 +0100
     3.2 +++ b/doc-src/IsarRef/Thy/document/Spec.tex	Fri Oct 15 19:19:41 2010 +0100
     3.3 @@ -859,11 +859,6 @@
     3.4      \indexdef{}{command}{attribute\_setup}\hypertarget{command.attribute-setup}{\hyperlink{command.attribute-setup}{\mbox{\isa{\isacommand{attribute{\isacharunderscore}setup}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     3.5    \end{matharray}
     3.6  
     3.7 -  \begin{mldecls}
     3.8 -    \indexdef{}{ML}{bind\_thms}\verb|bind_thms: string * thm list -> unit| \\
     3.9 -    \indexdef{}{ML}{bind\_thm}\verb|bind_thm: string * thm -> unit| \\
    3.10 -  \end{mldecls}
    3.11 -
    3.12    \begin{rail}
    3.13      'use' name
    3.14      ;
    3.15 @@ -951,21 +946,6 @@
    3.16  %
    3.17  \endisadelimML
    3.18  %
    3.19 -\begin{isamarkuptext}%
    3.20 -\begin{description}
    3.21 -
    3.22 -  \item \verb|bind_thms|~\isa{{\isachardoublequote}{\isacharparenleft}name{\isacharcomma}\ thms{\isacharparenright}{\isachardoublequote}} stores a list of
    3.23 -  theorems produced in ML both in the theory context and the ML
    3.24 -  toplevel, associating it with the provided name.  Theorems are put
    3.25 -  into a global ``standard'' format before being stored.
    3.26 -
    3.27 -  \item \verb|bind_thm| is similar to \verb|bind_thms| but refers to a
    3.28 -  singleton theorem.
    3.29 -  
    3.30 -  \end{description}%
    3.31 -\end{isamarkuptext}%
    3.32 -\isamarkuptrue%
    3.33 -%
    3.34  \isamarkupsection{Primitive specification elements%
    3.35  }
    3.36  \isamarkuptrue%