equal
deleted
inserted
replaced
1305 |
1305 |
1306 |
1306 |
1307 (** method setup **) |
1307 (** method setup **) |
1308 |
1308 |
1309 val blast_method = |
1309 val blast_method = |
1310 Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option Args.nat)) |
1310 Method.bang_sectioned_args' Data.cla_modifiers (Scan.lift (Scan.option OuterParse.nat)) |
1311 (fn NONE => Data.cla_meth' blast_tac |
1311 (fn NONE => Data.cla_meth' blast_tac |
1312 | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim)); |
1312 | SOME lim => Data.cla_meth' (fn cs => depth_tac cs lim)); |
1313 |
1313 |
1314 val setup = |
1314 val setup = |
1315 setup_depth_limit #> |
1315 setup_depth_limit #> |