diff -r e19d5b459a61 -r 4120fc59dd85 src/FOL/ex/Iff_Oracle.thy --- a/src/FOL/ex/Iff_Oracle.thy Fri Mar 13 19:53:09 2009 +0100 +++ b/src/FOL/ex/Iff_Oracle.thy Fri Mar 13 19:58:26 2009 +0100 @@ -53,7 +53,7 @@ method_setup iff = {* Method.simple_args OuterParse.nat (fn n => fn ctxt => - Method.SIMPLE_METHOD + SIMPLE_METHOD (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n))) handle Fail _ => no_tac)) *} "iff oracle"