ProgTutorial/Recipes/ExternalSolver.thy
changeset 562 daf404920ab9
parent 517 d8c376662bb4
child 565 cecd7a941885
--- a/ProgTutorial/Recipes/ExternalSolver.thy	Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Recipes/ExternalSolver.thy	Tue May 14 11:10:53 2019 +0200
@@ -28,8 +28,8 @@
   one second:
 
   @{ML_response_fake [display,gray] 
-    "TimeLimit.timeLimit (Time.fromSeconds 1) Isabelle_System.bash_output \"sleep 30\"
-     handle TimeLimit.TimeOut => (\"timeout\", ~1)" "(\"timeout\", ~1)"}
+    "Timeout.apply (Time.fromSeconds 1) Isabelle_System.bash_output \"sleep 30\"
+     handle TIMEOUT => (\"timeout\", ~1)" "(\"timeout\", ~1)"}
 
   The function @{ML bash_output in Isabelle_System} can also be used for more reasonable
   applications, e.g. coupling external solvers with Isabelle. In that case,