# HG changeset patch
# User haftmann
# Date 1200998248 -3600
# Node ID 6942f3c5dec882ab85abd524f7ed7990560c6726
# Parent  ddea202704b4813210fc8ae32de73bd4a3c0ccd7
avoid 'it' in ML expressions

diff -r ddea202704b4 -r 6942f3c5dec8 src/FOL/ex/IffOracle.thy
--- a/src/FOL/ex/IffOracle.thy	Mon Jan 21 14:18:49 2008 +0100
+++ b/src/FOL/ex/IffOracle.thy	Tue Jan 22 11:37:28 2008 +0100
@@ -35,7 +35,6 @@
 
 ML {* iff_oracle @{theory} 2 *}
 ML {* iff_oracle @{theory} 10 *}
-ML {* #der (Thm.rep_thm it) *}
 
 text {* These oracle calls had better fail. *}