--- a/ProgTutorial/Recipes/ExternalSolver.thy	Wed Oct 14 12:33:38 2009 +0200
+++ b/ProgTutorial/Recipes/ExternalSolver.thy	Wed Oct 14 14:56:19 2009 +0200
@@ -27,12 +27,10 @@
   properly. For example, the following expression takes only approximately
   one second:
 
-  @{ML_response [display,gray] 
+  @{ML_response_fake [display,gray] 
     "TimeLimit.timeLimit (Time.fromSeconds 1) system_out \"sleep 30\"
      handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"}
-*}
 
-text {*
   The function @{ML system_out} 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.