src/FOL/ex/Iff_Oracle.thy
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))