--- a/ProgTutorial/Recipes/ExternalSolver.thy	Thu Feb 11 10:44:50 2010 +0100
+++ b/ProgTutorial/Recipes/ExternalSolver.thy	Sun Mar 07 21:15:05 2010 +0100
@@ -10,7 +10,7 @@
   You want to use an external application.
   \smallskip
 
-  {\bf Solution:} The function @{ML system_out} might be the right thing for
+  {\bf Solution:} The function @{ML bash_output} might be the right thing for
   you.
   \smallskip
 
@@ -20,7 +20,7 @@
   For example, consider running an ordinary shell commands:
 
   @{ML_response [display,gray] 
-    "system_out \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"}
+    "bash_output \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"}
 
   Note that it works also fine with timeouts (see Recipe~\ref{rec:timeout}
   on Page~\pageref{rec:timeout}), i.e. external applications are killed
@@ -28,10 +28,10 @@
   one second:
 
   @{ML_response_fake [display,gray] 
-    "TimeLimit.timeLimit (Time.fromSeconds 1) system_out \"sleep 30\"
+    "TimeLimit.timeLimit (Time.fromSeconds 1) bash_output \"sleep 30\"
      handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"}
 
-  The function @{ML system_out} can also be used for more reasonable
+  The function @{ML bash_output} can also be used for more reasonable
   applications, e.g. coupling external solvers with Isabelle. In that case,
   one has to make sure that Isabelle can find the particular executable.
   One way to ensure this is by adding a Bash-like variable binding into
@@ -46,7 +46,7 @@
 
   In Isabelle, this application may now be executed by
 
-  @{ML_response_fake [display,gray] "system_out \"$FOO\"" "\<dots>"}
+  @{ML_response_fake [display,gray] "bash_output \"$FOO\"" "\<dots>"}
 *}