diff -r 3bd1aa2f3517 -r 686a7d71ed7b src/HOL/Examples/Iff_Oracle.thy
--- a/src/HOL/Examples/Iff_Oracle.thy	Tue Apr 18 11:58:12 2023 +0200
+++ b/src/HOL/Examples/Iff_Oracle.thy	Tue Apr 18 12:04:41 2023 +0200
@@ -36,8 +36,7 @@
 ML \<open>iff_oracle (\<^theory>, 10)\<close>
 
 ML \<open>
-  \<^assert> (map (#1 o #1) (Oracles.dest (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)])) =
-    [\<^oracle_name>\<open>iff_oracle\<close>]);
+  \<^assert> (map (#1 o #1) (Thm_Deps.all_oracles [iff_oracle (\<^theory>, 10)]) = [\<^oracle_name>\<open>iff_oracle\<close>]);
 \<close>
 
 text \<open>These oracle calls had better fail.\<close>