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