diff -r be23597e81db -r f875a25aa72d ProgTutorial/Intro.thy
--- a/ProgTutorial/Intro.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Intro.thy	Fri May 17 10:38:01 2019 +0200
@@ -152,7 +152,7 @@
   \begin{isabelle}
   \begin{graybox}
   \isacommand{ML}~\<open>\<verbopen>\<close>\isanewline
-  \hspace{5mm}@{ML "3 + 4"}\isanewline
+  \hspace{5mm}@{ML \<open>3 + 4\<close>}\isanewline
   \<open>\<verbclose>\<close>
   \end{graybox}
   \end{isabelle}
@@ -163,13 +163,13 @@
   the enclosing \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close> and just
   write:
 
-  @{ML [display,gray] "3 + 4"}
+  @{ML [display,gray] \<open>3 + 4\<close>}
   
   Whenever appropriate we also show the response the code 
   generates when evaluated. This response is prefixed with a 
   @{text [quotes] ">"}, like:
 
-  @{ML_matchresult [display,gray] "3 + 4" "7"}
+  @{ML_matchresult [display,gray] \<open>3 + 4\<close> \<open>7\<close>}
 
   The user-level commands of Isabelle (i.e., the non-ML code) are written
   in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply},