diff -r be23597e81db -r f875a25aa72d ProgTutorial/Recipes/ExternalSolver.thy
--- a/ProgTutorial/Recipes/ExternalSolver.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/ExternalSolver.thy	Fri May 17 10:38:01 2019 +0200
@@ -20,7 +20,7 @@
   For example, consider running an ordinary shell commands:
 
   @{ML_matchresult [display,gray] 
-    "Isabelle_System.bash_output \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"}
+    \<open>Isabelle_System.bash_output "echo Hello world!"\<close> \<open>("Hello world!\n", 0)\<close>}
 
   Note that it works also fine with timeouts (see Recipe~\ref{rec:timeout}
   on Page~\pageref{rec:timeout}), i.e. external applications are killed
@@ -28,8 +28,8 @@
   one second:
 
   @{ML_matchresult_fake [display,gray] 
-    "Timeout.apply (Time.fromSeconds 1) Isabelle_System.bash_output \"sleep 30\"
-     handle TIMEOUT => (\"timeout\", ~1)" "(\"timeout\", ~1)"}
+    \<open>Timeout.apply (Time.fromSeconds 1) Isabelle_System.bash_output "sleep 30"
+     handle TIMEOUT => ("timeout", ~1)\<close> \<open>("timeout", ~1)\<close>}
 
   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,
@@ -46,7 +46,7 @@
 
   In Isabelle, this application may now be executed by
 
-  @{ML_matchresult_fake [display,gray] "Isabelle_System.bash_output \"$FOO\"" "\<dots>"}
+  @{ML_matchresult_fake [display,gray] \<open>Isabelle_System.bash_output "$FOO"\<close> \<open>\<dots>\<close>}
 \<close>