--- a/ProgTutorial/Recipes/Oracle.thy	Tue May 14 17:45:13 2019 +0200
+++ b/ProgTutorial/Recipes/Oracle.thy	Thu May 16 19:56:12 2019 +0200
@@ -76,19 +76,19 @@
 text \<open>
   Here is the string representation of the term @{term "p = (q = p)"}:
 
-  @{ML_response 
+  @{ML_matchresult 
     "translate @{term \"p = (q = p)\"}" 
     "\" ( p <=> ( q <=> p ) ) \""}
 
   Let us check, what the solver returns when given a tautology:
 
-  @{ML_response 
+  @{ML_matchresult 
     "IffSolver.decide (translate @{term \"p = (q = p) = q\"})"
     "true"}
 
   And here is what it returns for a formula which is not valid:
 
-  @{ML_response 
+  @{ML_matchresult 
     "IffSolver.decide (translate @{term \"p = (q = p)\"})" 
     "false"}
 \<close>
@@ -113,7 +113,7 @@
 text \<open>
   Here is what we get when applying the oracle:
 
-  @{ML_response_fake "iff_oracle @{cprop \"p = (p::bool)\"}" "p = p"}
+  @{ML_matchresult_fake "iff_oracle @{cprop \"p = (p::bool)\"}" "p = p"}
 
   (FIXME: is there a better way to present the theorem?)