avoid 'it' in ML expressions
authorhaftmann
Tue, 22 Jan 2008 11:37:28 +0100
changeset 25940 6942f3c5dec8
parent 25939 ddea202704b4
child 25941 0929d6d08dd3
avoid 'it' in ML expressions
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. *}