diff -r be23597e81db -r f875a25aa72d ProgTutorial/Recipes/TimeLimit.thy
--- a/ProgTutorial/Recipes/TimeLimit.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/TimeLimit.thy	Fri May 17 10:38:01 2019 +0200
@@ -21,25 +21,25 @@
 
   Now the call 
 
-  @{ML_matchresult_fake_both [display,gray] "ackermann (4, 12)" "\<dots>"}
+  @{ML_matchresult_fake_both [display,gray] \<open>ackermann (4, 12)\<close> \<open>\<dots>\<close>}
 
   takes a bit of time before it finishes. To avoid this, the call can be encapsulated 
   in a time limit of five seconds. For this you have to write
 
 @{ML_matchresult_fake_both [display,gray]
-"Timeout.apply (Time.fromSeconds 5) ackermann (4, 12) 
-  handle TIMEOUT => ~1"
-"~1"}
+\<open>Timeout.apply (Time.fromSeconds 5) ackermann (4, 12) 
+  handle TIMEOUT => ~1\<close>
+\<open>~1\<close>}
 
   where \<open>TimeOut\<close> is the exception raised when the time limit
   is reached.
 
-  Note that @{ML  "apply" in Timeout} is only meaningful when you use PolyML 5.2.1
+  Note that @{ML \<open>apply\<close> in Timeout} is only meaningful when you use PolyML 5.2.1
   or later, because this version of PolyML has the infrastructure for multithreaded 
-  programming on which @{ML "apply" in Timeout} relies.
+  programming on which @{ML \<open>apply\<close> in Timeout} relies.
 
 \begin{readmore}
-   The function @{ML "apply" in Timeout} is defined in the structure
+   The function @{ML \<open>apply\<close> in Timeout} is defined in the structure
   @{ML_structure Timeout} which can be found in the file 
   @{ML_file "Pure/concurrent/timeout.ML"}.
 \end{readmore}