diff -r 3db1bbc82d8d -r 21c10672633b src/Doc/IsarImplementation/Integration.thy
--- 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.