src/Provers/blast.ML
changeset 36960 01594f816e3a
parent 36787 f60e4dd6d76f
child 41491 a2ad5b824051
--- a/src/Provers/blast.ML	Mon May 17 15:11:25 2010 +0200
+++ b/src/Provers/blast.ML	Mon May 17 23:54:15 2010 +0200
@@ -1309,7 +1309,7 @@
 val setup =
   setup_depth_limit #>
   Method.setup @{binding blast}
-    (Scan.lift (Scan.option OuterParse.nat) --| Method.sections Data.cla_modifiers >>
+    (Scan.lift (Scan.option Parse.nat) --| Method.sections Data.cla_modifiers >>
       (fn NONE => Data.cla_meth' blast_tac
         | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim)))
     "classical tableau prover";