# HG changeset patch
# User wenzelm
# Date 1201125427 -3600
# Node ID 8ceff6c1f2a83f47b5777fda74a9cc049cd896a8
# Parent  ddc6a331263695c94b230b463239d2d078f85242
recovered #der example without using val it;

diff -r ddc6a3312636 -r 8ceff6c1f2a8 src/FOL/ex/IffOracle.thy
--- a/src/FOL/ex/IffOracle.thy	Wed Jan 23 09:57:55 2008 +0100
+++ b/src/FOL/ex/IffOracle.thy	Wed Jan 23 22:57:07 2008 +0100
@@ -35,6 +35,7 @@
 
 ML {* iff_oracle @{theory} 2 *}
 ML {* iff_oracle @{theory} 10 *}
+ML {* #der (Thm.rep_thm (iff_oracle @{theory} 10)) *}
 
 text {* These oracle calls had better fail. *}