| changeset 27809 | a1e409db516b |
| parent 26939 | 1035c89b4c02 |
| child 30187 | b92b3375e919 |
| child 30240 | 5b25fee0362c |
--- a/src/Provers/blast.ML Sat Aug 09 12:28:13 2008 +0200 +++ b/src/Provers/blast.ML Sat Aug 09 22:43:46 2008 +0200 @@ -1307,7 +1307,7 @@ (** method setup **) val blast_method = - Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option Args.nat)) + Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option OuterParse.nat)) (fn NONE => Data.cla_meth' blast_tac | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim));