diff -r be23597e81db -r f875a25aa72d ProgTutorial/Appendix.thy
--- a/ProgTutorial/Appendix.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Appendix.thy	Fri May 17 10:38:01 2019 +0200
@@ -13,7 +13,7 @@
 
   \begin{itemize}
   \item translations/print translations; 
-  @{ML "Proof_Context.print_syntax"}
+  @{ML \<open>Proof_Context.print_syntax\<close>}
   
   \item user space type systems (in the form that already exists)