1.1 --- a/src/Provers/blast.ML	Mon Aug 02 17:59:06 1999 +0200
     1.2 +++ b/src/Provers/blast.ML	Mon Aug 02 17:59:25 1999 +0200
     1.3 @@ -67,7 +67,8 @@
     1.4  		 uwrappers: (string * wrapper) list,
     1.5  		 safe0_netpair: netpair, safep_netpair: netpair,
     1.6  		 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair}
     1.7 -  val cla_method': (claset -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
     1.8 +  val cla_modifiers: (Args.T list -> (Proof.context attribute * Args.T list)) list
     1.9 +  val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
    1.10    end;
    1.11  
    1.12  
    1.13 @@ -1329,7 +1330,13 @@
    1.14  
    1.15  (** method setup **)
    1.16  
    1.17 -val setup = [Method.add_methods [("blast", Data.cla_method' blast_tac, "tableau prover")]];
    1.18 +val blast_args =
    1.19 +  Method.sectioned_args (K (Scan.lift (Scan.option Args.nat))) Data.cla_modifiers;
    1.20 +
    1.21 +fun blast_meth None = Data.cla_meth' blast_tac
    1.22 +  | blast_meth (Some lim) = Data.cla_meth' (fn cs => depth_tac cs lim);
    1.23 +
    1.24 +val setup = [Method.add_methods [("blast", blast_args blast_meth, "tableau prover")]];
    1.25  
    1.26  
    1.27  end;