# HG changeset patch
# User wenzelm
# Date 938258638 -7200
# Node ID 6381cd433a991fb18b9d891ed8b4a3d7614ee7a5
# Parent  7905a74eb068f330255b02f816b6097889f34d7f
simplified sectioned_args;

diff -r 7905a74eb068 -r 6381cd433a99 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;