diff -r 15041c7e51e4 -r 21c20c7d1932 src/FOL/ex/Iff_Oracle.thy
--- a/src/FOL/ex/Iff_Oracle.thy	Wed Mar 25 16:54:49 2009 +0100
+++ b/src/FOL/ex/Iff_Oracle.thy	Wed Mar 25 17:23:44 2009 +0100
@@ -34,7 +34,7 @@
 
 ML {* iff_oracle (@{theory}, 2) *}
 ML {* iff_oracle (@{theory}, 10) *}
-ML {* Thm.proof_of (iff_oracle (@{theory}, 10)) *}
+ML {* Thm.proof_body_of (iff_oracle (@{theory}, 10)) *}
 
 text {* These oracle calls had better fail. *}