--- a/src/Doc/IsarImplementation/Integration.thy Tue Apr 09 13:55:28 2013 +0200
+++ b/src/Doc/IsarImplementation/Integration.thy Tue Apr 09 15:29:25 2013 +0200
@@ -145,7 +145,6 @@
text %mlref {*
\begin{mldecls}
@{index_ML Toplevel.print: "Toplevel.transition -> Toplevel.transition"} \\
- @{index_ML Toplevel.no_timing: "Toplevel.transition -> Toplevel.transition"} \\
@{index_ML Toplevel.keep: "(Toplevel.state -> unit) ->
Toplevel.transition -> Toplevel.transition"} \\
@{index_ML Toplevel.theory: "(theory -> theory) ->
@@ -166,10 +165,6 @@
causes the toplevel loop to echo the result state (in interactive
mode).
- \item @{ML Toplevel.no_timing}~@{text "tr"} indicates that the
- transition should never show timing information, e.g.\ because it is
- a diagnostic command.
-
\item @{ML Toplevel.keep}~@{text "tr"} adjoins a diagnostic
function.