--- a/ProgTutorial/Helper/Command/Command.thy	Tue May 14 16:59:53 2019 +0200
+++ b/ProgTutorial/Helper/Command/Command.thy	Tue May 14 17:10:47 2019 +0200
@@ -4,7 +4,7 @@
          "foobar_goal" "foobar_prove" :: thy_goal
 begin
 
-ML {*
+ML \<open>
 let
    val do_nothing = Scan.succeed (Local_Theory.background_theory I)
 in
@@ -12,9 +12,9 @@
      "description of foobar" 
        do_nothing
 end
-*}
+\<close>
 
-ML {*
+ML \<open>
 let
   fun trace_prop str =
      Local_Theory.background_theory (fn lthy => (tracing str; lthy))
@@ -24,9 +24,9 @@
     "traces a proposition"
       trace_prop_parser
 end
-*}
+\<close>
 
-ML {*
+ML \<open>
 let
    fun prove_prop str lthy =
      let
@@ -40,17 +40,17 @@
      "proving a proposition"
        prove_prop_parser
 end
-*}
+\<close>
 
-ML {*
+ML \<open>
 structure Result = Proof_Data(
   type T = unit -> term
   fun init thy () = error "Result")
 
 val result_cookie = (Result.get, Result.put, "Result.put")
-*}
+\<close>
 
-ML{*
+ML\<open>
 let
    fun after_qed thm_name thms lthy =
         Local_Theory.note (thm_name, (flat thms)) lthy |> snd
@@ -68,7 +68,7 @@
    Outer_Syntax.local_theory_to_proof @{command_spec "foobar_prove"} 
      "proving a proposition" 
         (parser >> setup_proof)
-end*}
+end\<close>