diff -r aec7073d4645 -r daf404920ab9 ProgTutorial/Recipes/ExternalSolver.thy --- 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,