diff -r f5417836dbea -r 01594f816e3a src/Provers/blast.ML --- 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";