--- a/ProgTutorial/Recipes/Oracle.thy	Fri May 17 11:21:09 2019 +0200
+++ b/ProgTutorial/Recipes/Oracle.thy	Tue May 21 14:37:39 2019 +0200
@@ -110,7 +110,7 @@
 text \<open>
   Here is what we get when applying the oracle:
 
-  @{ML_matchresult_fake \<open>iff_oracle @{cprop "p = (p::bool)"}\<close> \<open>p = p\<close>}
+  @{ML_response \<open>iff_oracle @{cprop "p = (p::bool)"}\<close> \<open>p = p\<close>}
 
   (FIXME: is there a better way to present the theorem?)