diff -r 802576856527 -r 09e52d4a850a src/Doc/System/Misc.thy
--- a/src/Doc/System/Misc.thy	Sun Jul 07 18:34:29 2013 +0200
+++ b/src/Doc/System/Misc.thy	Sun Jul 07 18:43:14 2013 +0200
@@ -238,25 +238,6 @@
   using this template.  *}
 
 
-section {* Printing documents *}
-
-text {*
-  The @{tool_def print} tool prints documents:
-\begin{ttbox}
-Usage: isabelle print [OPTIONS] FILE
-
-  Options are:
-    -c           cleanup -- remove FILE after use
-
-  Print document FILE.
-\end{ttbox}
-
-  The @{verbatim "-c"} option causes the input file to be removed
-  after use.  The printer spool command is determined by the @{setting
-  PRINT_COMMAND} setting.
-*}
-
-
 section {* Remove awkward symbol names from theory sources *}
 
 text {*