# HG changeset patch
# User wenzelm
# Date 1237998224 -3600
# Node ID 21c20c7d1932284c420f48cd471736c4bc9f68d2
# Parent  15041c7e51e404ce7c23cb840769ff3fb7ceb517
use more informative Thm.proof_body_of for oracle demo;

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. *}