changeset 36960 | 01594f816e3a |
parent 30719 | 21c20c7d1932 |
--- a/src/FOL/ex/Iff_Oracle.thy Mon May 17 15:11:25 2010 +0200 +++ b/src/FOL/ex/Iff_Oracle.thy Mon May 17 23:54:15 2010 +0200 @@ -52,7 +52,7 @@ subsection {* Oracle as proof method *} method_setup iff = {* - Scan.lift OuterParse.nat >> (fn n => fn ctxt => + Scan.lift Parse.nat >> (fn n => fn ctxt => SIMPLE_METHOD (HEADGOAL (Tactic.rtac (iff_oracle (ProofContext.theory_of ctxt, n))) handle Fail _ => no_tac))