simplified sectioned_args;
authorwenzelm
Sat, 25 Sep 1999 13:23:58 +0200
changeset 7607 6381cd433a99
parent 7606 7905a74eb068
child 7608 8069542cba82
simplified sectioned_args;
src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sat Sep 25 13:20:12 1999 +0200
+++ b/src/Provers/blast.ML	Sat Sep 25 13:23:58 1999 +0200
@@ -1331,7 +1331,7 @@
 (** method setup **)
 
 fun blast_args m =
-  Method.sectioned_args (K (Args.bang_facts -- Scan.lift (Scan.option Args.nat))) Data.cla_modifiers m;
+  Method.sectioned_args (Args.bang_facts -- Scan.lift (Scan.option Args.nat)) Data.cla_modifiers m;
 
 fun blast_meth (prems, None) = Data.cla_meth' blast_tac prems
   | blast_meth (prems, Some lim) = Data.cla_meth' (fn cs => depth_tac cs lim) prems;