--- a/src/Doc/System/Environment.thy Mon Mar 30 19:39:11 2020 +0200
+++ b/src/Doc/System/Environment.thy Mon Mar 30 19:50:01 2020 +0200
@@ -390,8 +390,8 @@
\<^medskip>
This is how to invoke a function body with proper return code and printing
of errors, and without printing of a redundant \<^verbatim>\<open>val it = (): unit\<close> result:
- @{verbatim [display] \<open>isabelle process -e 'Command_Line.tool0 (fn () => writeln "OK")'\<close>}
- @{verbatim [display] \<open>isabelle process -e 'Command_Line.tool0 (fn () => error "Bad")'\<close>}
+ @{verbatim [display] \<open>isabelle process -e 'Command_Line.tool (fn () => writeln "OK")'\<close>}
+ @{verbatim [display] \<open>isabelle process -e 'Command_Line.tool (fn () => error "Bad")'\<close>}
\<close>