--- a/ProgTutorial/Package/Ind_Code.thy	Fri May 17 11:21:09 2019 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Tue May 21 14:37:39 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_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
 \<open>let
   val ctrms = [@{cterm "a::nat"}, @{cterm "b::nat"}, @{cterm "c::nat"}]
   val new_thm = all_elims ctrms @{thm all_elims_test}
@@ -510,13 +510,13 @@
   For example we can eliminate the preconditions \<open>A\<close> and \<open>B\<close> from
   @{thm [source] imp_elims_test}:
 
-  @{ML_matchresult_fake [display, gray]
+  @{ML_response [display, gray]
 \<open>let
   val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}
 in
   pwriteln (pretty_thm_no_vars @{context} res)
 end\<close>
-  \<open>C\<close>}
+  \<open>Q\<close>}
 
   Now we set up the proof for the introduction rule as follows:
 \<close>