--- a/ProgTutorial/Package/Ind_Code.thy	Tue May 14 17:45:13 2019 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Thu May 16 19:56:12 2019 +0200
@@ -493,7 +493,7 @@
   theorems of the form @{thm [source] all_elims_test}. For example we can instantiate
   the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows:
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
 "let
   val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}]
   val new_thm = all_elims ctrms @{thm all_elims_test}
@@ -510,7 +510,7 @@
   For example we can eliminate the preconditions \<open>A\<close> and \<open>B\<close> from
   @{thm [source] imp_elims_test}:
 
-  @{ML_response_fake [display, gray]
+  @{ML_matchresult_fake [display, gray]
 "let
   val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}
 in