src/Provers/blast.ML

                  swrappers: (string * wrapper) list,
                  uwrappers: (string * wrapper) list,
                  safe0_netpair: netpair, safep_netpair: netpair,
                  haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: Context_Rules.netpair}
   val cla_modifiers: Method.modifier parser list
-  val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
+  val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
 end;
 
 signature BLAST =
 sig
   type claset

 (** method setup **)
 
 val setup =
   setup_depth_limit #>
   Method.setup @{binding blast}
-    (Args.bang_facts -- Scan.lift (Scan.option OuterParse.nat) --|
-      Method.sections Data.cla_modifiers >>
-      (fn (prems, NONE) => Data.cla_meth' blast_tac prems
-        | (prems, SOME lim) => Data.cla_meth' (fn cs => depth_tac cs lim) prems))
+    (Scan.lift (Scan.option OuterParse.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";
 
 end;