diff -r 438703674711 -r 321e220a6baa ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Essential.thy	Tue May 21 16:22:30 2019 +0200
@@ -2098,10 +2098,10 @@
   Note also that applications of \<open>assumption\<close> do not
   count as a separate theorem, as you can see in the following code.
 
-  @{ML_matchresult [display,gray]
+  @{ML_response [display,gray]
   \<open>@{thm my_conjIb}
   |> get_all_names |> sort string_ord\<close>
-  \<open>["", "Pure.protectD", "Pure.protectI"]\<close>}
+  \<open>[ "Pure.protectD", "Pure.protectI"]\<close>}
 
 
   Interestingly, but not surprisingly, the proof of @{thm [source]