--- a/ProgTutorial/Advanced.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Advanced.thy	Fri May 17 10:38:01 2019 +0200
@@ -132,14 +132,13 @@
 
   \begin{isabelle}
   \begin{graybox}
-  \isacommand{setup}~\<open>\<verbopen>\<close> @{ML
-"fn thy => 
+  \isacommand{setup}~\<open>\<verbopen>\<close> @{ML \<open>fn thy => 
 let
-  val bar_const = ((@{binding \"BAR\"}, @{typ \"nat\"}), NoSyn)
+  val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn)
   val (_, thy') = Sign.declare_const @{context} bar_const thy
 in
   thy
-end"}~\<open>\<verbclose>\<close>\isanewline
+end\<close>}~\<open>\<verbclose>\<close>\isanewline
   \<open>> ERROR: "Stale theory encountered"\<close>
   \end{graybox}
   \end{isabelle}
@@ -215,14 +214,14 @@
 
   \begin{isabelle}
   \begin{graybox}
-  @{ML "let
-  val trm = @{term \"(x, y, z, w)\"}
+  @{ML \<open>let
+  val trm = @{term "(x, y, z, w)"}
 in
   pwriteln (Pretty.chunks 
     [ pretty_term ctxt0 trm,
       pretty_term ctxt1 trm,
       pretty_term ctxt2 trm ])
-end"}\\
+end\<close>}\\
   \setlength{\fboxsep}{0mm}
   \<open>>\<close>~\<open>(\<close>\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>x\<close>}}\<open>,\<close>~%
   \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>y\<close>}}\<open>,\<close>~%
@@ -241,9 +240,8 @@
 
 
   The term we are printing is in all three cases the same---a tuple containing
-  four free variables. As you can see, however, in case of @{ML "ctxt0"} all
-  variables are highlighted indicating a problem, while in case of @{ML
-  "ctxt1"} \<open>x\<close> and \<open>y\<close> are printed as normal (blue) free
+  four free variables. As you can see, however, in case of @{ML \<open>ctxt0\<close>} all
+  variables are highlighted indicating a problem, while in case of @{ML \<open>ctxt1\<close>} \<open>x\<close> and \<open>y\<close> are printed as normal (blue) free
   variables, but not \<open>z\<close> and \<open>w\<close>. In the last case all variables
   are printed as expected. The point of this example is that the context
   contains the information which variables are fixed, and designates all other
@@ -253,18 +251,18 @@
   fixing a variable twice
 
   @{ML_matchresult_fake [gray, display]
-  "@{context}
-|> Variable.add_fixes [\"x\", \"x\"]" 
-  "ERROR: Duplicate fixed variable(s): \"x\""}
+  \<open>@{context}
+|> Variable.add_fixes ["x", "x"]\<close> 
+  \<open>ERROR: Duplicate fixed variable(s): "x"\<close>}
 
   More importantly it also allows us to easily create fresh names for
   fixed variables.  For this you have to use the function @{ML_ind
   variant_fixes in Variable} from the structure @{ML_structure Variable}.
 
   @{ML_matchresult_fake [gray, display]
-  "@{context}
-|> Variable.variant_fixes [\"y\", \"y\", \"z\"]" 
-  "([\"y\", \"ya\", \"z\"], ...)"}
+  \<open>@{context}
+|> Variable.variant_fixes ["y", "y", "z"]\<close> 
+  \<open>(["y", "ya", "z"], ...)\<close>}
 
   Now a fresh variant for the second occurence of \<open>y\<close> is created
   avoiding any clash. In this way we can also create fresh free variables
@@ -274,16 +272,16 @@
   string @{text [quotes] "x"} (Lines 6 and 7).
 
   @{ML_matchresult_fake [display, gray, linenos]
-  "let
+  \<open>let
   val ctxt0 = @{context}
-  val (_, ctxt1) = Variable.add_fixes [\"x\"] ctxt0
-  val frees = replicate 2 (\"x\", @{typ nat})
+  val (_, ctxt1) = Variable.add_fixes ["x"] ctxt0
+  val frees = replicate 2 ("x", @{typ nat})
 in
   (Variable.variant_frees ctxt0 [] frees,
    Variable.variant_frees ctxt1 [] frees)
-end"
-  "([(\"x\", \"nat\"), (\"xa\", \"nat\")], 
- [(\"xa\", \"nat\"), (\"xb\", \"nat\")])"}
+end\<close>
+  \<open>([("x", "nat"), ("xa", "nat")], 
+ [("xa", "nat"), ("xb", "nat")])\<close>}
 
   As you can see, if we create the fresh variables with the context \<open>ctxt0\<close>,
   then we obtain \<open>x\<close> and \<open>xa\<close>; but in \<open>ctxt1\<close> we obtain \<open>xa\<close>
@@ -294,13 +292,13 @@
   function @{ML_ind declare_term in Variable} from the structure @{ML_structure Variable}.
 
   @{ML_matchresult_fake [gray, display]
-  "let
-  val ctxt1 = Variable.declare_term @{term \"(x, xa)\"} @{context}
-  val frees = replicate 2 (\"x\", @{typ nat})
+  \<open>let
+  val ctxt1 = Variable.declare_term @{term "(x, xa)"} @{context}
+  val frees = replicate 2 ("x", @{typ nat})
 in
   Variable.variant_frees ctxt1 [] frees
-end"
-  "[(\"xb\", \"nat\"), (\"xc\", \"nat\")]"}
+end\<close>
+  \<open>[("xb", "nat"), ("xc", "nat")]\<close>}
 
   The result is \<open>xb\<close> and \<open>xc\<close> for the names of the fresh
   variables, since \<open>x\<close> and \<open>xa\<close> occur in the term we declared. 
@@ -310,12 +308,12 @@
 
   \begin{isabelle}
   \begin{graybox}
-  @{ML "let
-  val trm = @{term \"P x y z\"}
+  @{ML \<open>let
+  val trm = @{term "P x y z"}
   val ctxt1 = Variable.declare_term trm @{context}
 in
   pwriteln (pretty_term ctxt1 trm)
-end"}\\
+end\<close>}\\
   \setlength{\fboxsep}{0mm}
   \<open>>\<close>~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>P\<close>}}~%
   \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>x\<close>}}~%
@@ -330,14 +328,14 @@
   @{ML_structure Syntax}. Consider the following code:
 
   @{ML_matchresult_fake [gray, display]
-  "let
+  \<open>let
   val ctxt0 = @{context}
-  val ctxt1 = Variable.declare_term @{term \"x::nat\"} ctxt0
+  val ctxt1 = Variable.declare_term @{term "x::nat"} ctxt0
 in
-  (Syntax.read_term ctxt0 \"x\", 
-   Syntax.read_term ctxt1 \"x\") 
-end"
-  "(Free (\"x\", \"'a\"), Free (\"x\", \"nat\"))"}
+  (Syntax.read_term ctxt0 "x", 
+   Syntax.read_term ctxt1 "x") 
+end\<close>
+  \<open>(Free ("x", "'a"), Free ("x", "nat"))\<close>}
   
   Parsing the string in the context \<open>ctxt0\<close> results in a free variable 
   with a default polymorphic type, but in case of \<open>ctxt1\<close> we obtain a
@@ -346,14 +344,14 @@
   is made, as the next example illustrates.
 
   @{ML_matchresult_fake [gray, display]
-  "let
-  val ctxt1 = Variable.declare_term @{term \"x::nat\"} @{context}
-  val ctxt2 = Variable.declare_term @{term \"x::int\"} ctxt1
+  \<open>let
+  val ctxt1 = Variable.declare_term @{term "x::nat"} @{context}
+  val ctxt2 = Variable.declare_term @{term "x::int"} ctxt1
 in
-  (Syntax.read_term ctxt1 \"x\", 
-   Syntax.read_term ctxt2 \"x\") 
-end"
-  "(Free (\"x\", \"nat\"), Free (\"x\", \"int\"))"}
+  (Syntax.read_term ctxt1 "x", 
+   Syntax.read_term ctxt2 "x") 
+end\<close>
+  \<open>(Free ("x", "nat"), Free ("x", "int"))\<close>}
 
   The most useful feature of contexts is that one can export, or transfer, 
   terms and theorems between them. We show this first for terms. 
@@ -361,15 +359,15 @@
   \begin{isabelle}
   \begin{graybox}
   \begin{linenos}
-  @{ML "let
+  @{ML \<open>let
   val ctxt0 = @{context}
-  val (_, ctxt1) = Variable.add_fixes [\"x\", \"y\", \"z\"] ctxt0 
-  val foo_trm = @{term \"P x y z\"}
+  val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0 
+  val foo_trm = @{term "P x y z"}
 in
   singleton (Variable.export_terms ctxt1 ctxt0) foo_trm
   |> pretty_term ctxt0
   |> pwriteln
-end"}
+end\<close>}
   \end{linenos}
   \setlength{\fboxsep}{0mm}
   \<open>>\<close>~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>P\<close>}}~%
@@ -401,15 +399,15 @@
   whether it is actually provable).
 
   @{ML_matchresult_fake [display, gray]
-  "let
+  \<open>let
   val thy = @{theory}
   val ctxt0 = @{context}
-  val (_, ctxt1) = Variable.add_fixes [\"P\", \"x\", \"y\", \"z\"] ctxt0 
-  val foo_thm = Skip_Proof.make_thm thy @{prop \"P x y z x y z\"}
+  val (_, ctxt1) = Variable.add_fixes ["P", "x", "y", "z"] ctxt0 
+  val foo_thm = Skip_Proof.make_thm thy @{prop "P x y z x y z"}
 in
   singleton (Proof_Context.export ctxt1 ctxt0) foo_thm
-end"
-  "?P ?x ?y ?z ?x ?y ?z"}
+end\<close>
+  \<open>?P ?x ?y ?z ?x ?y ?z\<close>}
 
   Since we fixed all variables in \<open>ctxt1\<close>, in the exported
   result all of them are schematic. The great point of contexts is
@@ -419,14 +417,14 @@
   @{ML_structure Assumption}. Consider the following code.
 
   @{ML_matchresult_fake [display, gray, linenos]
-  "let
+  \<open>let
   val ctxt0 = @{context}
-  val ([eq], ctxt1) = Assumption.add_assumes [@{cprop \"x \<equiv> y\"}] ctxt0
+  val ([eq], ctxt1) = Assumption.add_assumes [@{cprop "x \<equiv> y"}] ctxt0
   val eq' = Thm.symmetric eq
 in
   Assumption.export false ctxt1 ctxt0 eq'
-end"
-  "x \<equiv> y \<Longrightarrow> y \<equiv> x"}
+end\<close>
+  \<open>x \<equiv> y \<Longrightarrow> y \<equiv> x\<close>}
   
   The function @{ML_ind add_assumes in Assumption} from the structure
   @{ML_structure Assumption} adds the assumption \mbox{\<open>x \<equiv> y\<close>}
@@ -451,16 +449,16 @@
   in the following example.
 
   @{ML_matchresult_fake [display, gray]
-  "let
+  \<open>let
   val ctxt0 = @{context}
   val ((fvs, [eq]), ctxt1) = ctxt0
-    |> Variable.add_fixes [\"x\", \"y\"]
-    ||>> Assumption.add_assumes [@{cprop \"x \<equiv> y\"}]
+    |> Variable.add_fixes ["x", "y"]
+    ||>> Assumption.add_assumes [@{cprop "x \<equiv> y"}]
   val eq' = Thm.symmetric eq
 in
   Proof_Context.export ctxt1 ctxt0 [eq']
-end"
-  "[?x \<equiv> ?y \<Longrightarrow> ?y \<equiv> ?x]"}
+end\<close>
+  \<open>[?x \<equiv> ?y \<Longrightarrow> ?y \<equiv> ?x]\<close>}
 \<close>
 
 
@@ -515,7 +513,7 @@
   @{ML_type "Proof.context"}, although not every proof context constitutes a
   valid local theory.
 
-  @{ML "Context.>> o Context.map_theory"}
+  @{ML \<open>Context.>> o Context.map_theory\<close>}
   @{ML_ind "Local_Theory.declaration"}
 
    A similar command is \isacommand{local\_setup}, which expects a function
@@ -590,8 +588,8 @@
   antiquotation \<open>@{binding \<dots>}\<close>. For example
 
   @{ML_matchresult [display,gray]
-  "@{binding \"name\"}"
-  "name"}
+  \<open>@{binding "name"}\<close>
+  \<open>name\<close>}
 
   An example where a qualified name is needed is the function 
   @{ML_ind define in Local_Theory}.  This function is used below to define 
@@ -634,7 +632,7 @@
   Occasionally you have to calculate what the ``base'' name of a given
   constant is. For this you can use the function @{ML_ind  Long_Name.base_name}. For example:
 
-  @{ML_matchresult [display,gray] "Long_Name.base_name \"List.list.Nil\"" "\"Nil\""}
+  @{ML_matchresult [display,gray] \<open>Long_Name.base_name "List.list.Nil"\<close> \<open>"Nil"\<close>}
 
   \begin{readmore}
   Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};