| changeset 30719 | 21c20c7d1932 |
| parent 30549 | d2d7874648bd |
| child 36960 | 01594f816e3a |
--- 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. *}