diff -r be23597e81db -r f875a25aa72d ProgTutorial/Recipes/Timing.thy
--- a/ProgTutorial/Recipes/Timing.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/Timing.thy	Fri May 17 10:38:01 2019 +0200
@@ -41,7 +41,7 @@
   tactics are lazy functions and you need to force them to run, otherwise the
   timing will be meaningless. The simplifier tactic, amongst others,  can be 
   forced to run by just applying the state to it. But ``fully'' lazy tactics,
-  such as @{ML "resolve_tac"}, need even more ``standing-on-ones-head'' to force
+  such as @{ML \<open>resolve_tac\<close>}, need even more ``standing-on-ones-head'' to force
   them to run. 
 
   The time between start and finish of the simplifier will be calculated