diff -r be23597e81db -r f875a25aa72d ProgTutorial/Recipes/Oracle.thy
--- a/ProgTutorial/Recipes/Oracle.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/Oracle.thy	Fri May 17 10:38:01 2019 +0200
@@ -76,21 +76,18 @@
 text \<open>
   Here is the string representation of the term @{term "p = (q = p)"}:
 
-  @{ML_matchresult 
-    "translate @{term \"p = (q = p)\"}" 
-    "\" ( p <=> ( q <=> p ) ) \""}
+  @{ML_matchresult \<open>translate @{term "p = (q = p)"}\<close> 
+    \<open>" ( p <=> ( q <=> p ) ) "\<close>}
 
   Let us check, what the solver returns when given a tautology:
 
-  @{ML_matchresult 
-    "IffSolver.decide (translate @{term \"p = (q = p) = q\"})"
-    "true"}
+  @{ML_matchresult \<open>IffSolver.decide (translate @{term "p = (q = p) = q"})\<close>
+    \<open>true\<close>}
 
   And here is what it returns for a formula which is not valid:
 
-  @{ML_matchresult 
-    "IffSolver.decide (translate @{term \"p = (q = p)\"})" 
-    "false"}
+  @{ML_matchresult \<open>IffSolver.decide (translate @{term "p = (q = p)"})\<close> 
+    \<open>false\<close>}
 \<close>
 
 text \<open>
@@ -113,7 +110,7 @@
 text \<open>
   Here is what we get when applying the oracle:
 
-  @{ML_matchresult_fake "iff_oracle @{cprop \"p = (p::bool)\"}" "p = p"}
+  @{ML_matchresult_fake \<open>iff_oracle @{cprop "p = (p::bool)"}\<close> \<open>p = p\<close>}
 
   (FIXME: is there a better way to present the theorem?)