diff -r be23597e81db -r f875a25aa72d ProgTutorial/Readme.thy
--- a/ProgTutorial/Readme.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Readme.thy	Fri May 17 10:38:01 2019 +0200
@@ -39,7 +39,7 @@
   The following antiquotations are defined:
 
   \begin{itemize}
-  \item[$\bullet$] \<open>@{ML "expr" for vars in structs}\<close> should be used
+  \item[$\bullet$] \<open>@{ML \<open>expr\<close> for vars in structs}\<close> should be used
   for displaying any ML-ex\-pression, because the antiquotation checks whether
   the expression is valid ML-code. The \<open>for\<close>- and \<open>in\<close>-arguments are optional. The former is used for evaluating open
   expressions by giving a list of free variables. The latter is used to
@@ -48,23 +48,23 @@
   
   \begin{center}\small
   \begin{tabular}{lll}
-  \<open>@{ML "1 + 3"}\<close>         &                 & @{ML "1 + 3"}\\
-  \<open>@{ML "a + b" for a b}\<close> & \;\;produce\;\; & @{ML "a + b" for a b}\\
-  \<open>@{ML Ident in OuterLex}\<close> &                 & @{ML Ident in OuterLex}\\
+  \<open>@{ML \<open>1 + 3\<close>}\<close>         &                 & @{ML \<open>1 + 3\<close>}\\
+  \<open>@{ML \<open>a + b\<close> for a b}\<close> & \;\;produce\;\; & @{ML \<open>a + b\<close> for a b}\\
+  \<open>@{ML explode in Symbol}\<close> &                 & @{ML explode in Symbol}\\
   \end{tabular}
   \end{center}
 
-  \item[$\bullet$] \<open>@{ML_matchresult "expr" "pat"}\<close> should be used to
+  \item[$\bullet$] \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close> should be used to
   display ML-expressions and their response.  The first expression is checked
-  like in the antiquotation \<open>@{ML "expr"}\<close>; the second is a pattern
+  like in the antiquotation \<open>@{ML \<open>expr\<close>}\<close>; the second is a pattern
   that specifies the result the first expression produces. This pattern can
   contain @{text [quotes] "\<dots>"} for parts that you like to omit. The response of the
   first expression will be checked against this pattern. Examples are:
 
   \begin{center}\small
   \begin{tabular}{l}
-  \<open>@{ML_matchresult "1+2" "3"}\<close>\\
-  \<open>@{ML_matchresult "(1+2,3)" "(3,\<dots>)"}\<close>
+  \<open>@{ML_matchresult \<open>1+2\<close> \<open>3\<close>}\<close>\\
+  \<open>@{ML_matchresult \<open>(1+2,3)\<close> \<open>(3,\<dots>)\<close>}\<close>
   \end{tabular}
   \end{center}
 
@@ -72,8 +72,8 @@
 
   \begin{center}\small
   \begin{tabular}{p{3cm}p{3cm}}
-  @{ML_matchresult "1+2" "3"} &  
-  @{ML_matchresult "(1+2,3)" "(3,\<dots>)"}
+  @{ML_matchresult \<open>1+2\<close> \<open>3\<close>} &  
+  @{ML_matchresult \<open>(1+2,3)\<close> \<open>(3,_)\<close>}
   \end{tabular}
   \end{center}
   
@@ -82,16 +82,16 @@
   an abstract datatype (like @{ML_type thm} or @{ML_type cterm}).
 
   \item[$\bullet$] \<open>@{ML_matchresult_fake "expr" "pat"}\<close> works just
-  like the antiquotation \<open>@{ML_matchresult "expr" "pat"}\<close> above,
+  like the antiquotation \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close> above,
   except that the result-specification is not checked. Use this antiquotation
   when the result cannot be constructed or the code generates an
   exception. Examples are:
 
   \begin{center}\small
   \begin{tabular}{ll}
-  \<open>@{ML_matchresult_fake\<close> & \<open>"cterm_of @{theory} @{term \"a + b = c\"}"}\<close>\\
+  \<open>@{ML_matchresult_fake\<close> & \<open>"cterm_of @{theory} @{term "a + b = c"}"}\<close>\\
                                & \<open>"a + b = c"}\<close>\smallskip\\ 
-  \<open>@{ML_matchresult_fake\<close> & \<open>"($$ \"x\") (explode \"world\")"\<close>\\ 
+  \<open>@{ML_matchresult_fake\<close> & \<open>"($$ "x") (explode "world")"\<close>\\ 
                                & \<open>"Exception FAIL raised"}\<close>
   \end{tabular}
   \end{center}
@@ -100,8 +100,8 @@
 
   \begin{center}\small
   \begin{tabular}{p{7.2cm}}
-  @{ML_matchresult_fake "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}\smallskip\\
-  @{ML_matchresult_fake "($$ \"x\") (explode \"world\")" "Exception FAIL raised"}
+  @{ML_matchresult_fake \<open>Thm.cterm_of @{context} @{term "a + b = c"}\<close> \<open>a + b = c\<close>}\smallskip\\
+  @{ML_matchresult_fake \<open>($$ "x") (Symbol.explode "world")\<close> \<open>Exception FAIL raised\<close>}
   \end{tabular}
   \end{center}
   
@@ -114,7 +114,7 @@
 
   \begin{center}\small
   \begin{tabular}{ll}
-  \<open>@{ML_matchresult_fake_both\<close> & \<open>"@{cterm \"1 + True\"}"\<close>\\
+  \<open>@{ML_matchresult_fake_both\<close> & \<open>"@{cterm "1 + True"}"\<close>\\
                                     & \<open>"Type unification failed \<dots>"}\<close>
   \end{tabular}
   \end{center}
@@ -123,20 +123,20 @@
   referring to a file. It checks whether the file exists.  An example
   is 
 
-  @{text [display] "@{ML_file \"Pure/General/basics.ML\"}"}
+  @{text [display] \<open>@{ML_file "Pure/General/basics.ML"}\<close>}
   \end{itemize}
 
   The listed antiquotations honour options including \<open>[display]\<close> and 
   \<open>[quotes]\<close>. For example
 
   \begin{center}\small
-  \<open>@{ML [quotes] "\"foo\" ^ \"bar\""}\<close> \;\;produces\;\; @{text [quotes] "foobar"}
+  \<open>@{ML [quotes] \<open>"foo" ^ "bar"\<close>}\<close> \;\;produces\;\; @{text [quotes] "foobar"}
   \end{center}
 
   whereas
   
   \begin{center}\small
-  \<open>@{ML "\"foo\" ^ \"bar\""}\<close> \;\;produces only\;\; \<open>foobar\<close>
+  \<open>@{ML \<open>"foo" ^ "bar"\<close>}\<close> \;\;produces only\;\; \<open>foobar\<close>
   \end{center}
   
   \item Functions and value bindings cannot be defined inside antiquotations; they need