--- a/ProgTutorial/Base.thy	Tue May 14 16:59:53 2019 +0200
+++ b/ProgTutorial/Base.thy	Tue May 14 17:10:47 2019 +0200
@@ -12,7 +12,7 @@
 notation (latex output)
   Cons ("_ # _" [66,65] 65)
 
-ML %linenosgrayML{*fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) 
+ML %linenosgrayML\<open>fun P n = @{term "P::nat \<Rightarrow> bool"} $ (HOLogic.mk_number @{typ "nat"} n) 
 
 fun rhs 1 = P 1
   | rhs n = HOLogic.mk_conj (P n, rhs (n - 1))
@@ -22,14 +22,14 @@
                  (HOLogic.mk_eq (P (m - 1), P m), rhs n), lhs (m - 1) n)
 
 fun de_bruijn n =
-  HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))*}
+  HOLogic.mk_Trueprop (HOLogic.mk_imp (lhs n n, rhs n))\<close>
 
 ML_file "output_tutorial.ML"
 ML_file "antiquote_setup.ML"
 
 
 (*setup {* OutputTutorial.setup *}*) (* Seems to be standard now, we don't need this anymoe *)
-setup {* AntiquoteSetup.setup *}
+setup \<open>AntiquoteSetup.setup\<close>
 
 print_ML_antiquotations