# HG changeset patch
# User wenzelm
# Date 937927610 -7200
# Node ID 1d2c099e98f78fa9c8f166ef63205f073cc86a7a
# Parent  08b2d5c94b8a376bf46f5b3012a50d92f08c948a
setup for refined facts handling;
Method.bang_sectioned_args / Args.bang_facts;

diff -r 08b2d5c94b8a -r 1d2c099e98f7 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Tue Sep 21 17:26:42 1999 +0200
+++ b/src/Provers/blast.ML	Tue Sep 21 17:26:50 1999 +0200
@@ -68,7 +68,7 @@
 		 safe0_netpair: netpair, safep_netpair: netpair,
 		 haz_netpair: netpair, dup_netpair: netpair, xtra_netpair: netpair}
   val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
-  val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
+  val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
   end;
 
 
@@ -1330,11 +1330,11 @@
 
 (** method setup **)
 
-val blast_args =
-  Method.sectioned_args (K (Scan.lift (Scan.option Args.nat))) Data.cla_modifiers;
+fun blast_args m =
+  Method.sectioned_args (K (Args.bang_facts -- Scan.lift (Scan.option Args.nat))) Data.cla_modifiers m;
 
-fun blast_meth None = Data.cla_meth' blast_tac
-  | blast_meth (Some lim) = Data.cla_meth' (fn cs => depth_tac cs lim);
+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;
 
 val setup = [Method.add_methods [("blast", blast_args blast_meth, "tableau prover")]];
 
diff -r 08b2d5c94b8a -r 1d2c099e98f7 src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Tue Sep 21 17:26:42 1999 +0200
+++ b/src/Provers/clasimp.ML	Tue Sep 21 17:26:50 1999 +0200
@@ -153,16 +153,15 @@
   (Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
 
 val clasimp_modifiers = Classical.cla_modifiers @ Simplifier.simp_modifiers;
-val clasimp_args = Method.only_sectioned_args clasimp_modifiers;
 
-fun clasimp_meth tac ctxt = Method.METHOD (fn facts =>
-  ALLGOALS (Method.insert_tac facts) THEN tac (get_local_clasimpset ctxt));
+fun clasimp_meth tac prems ctxt = Method.METHOD (fn facts =>
+  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_clasimpset ctxt));
 
-fun clasimp_meth' tac ctxt = Method.METHOD (fn facts =>
-  FIRSTGOAL (Method.insert_tac facts THEN' tac (get_local_clasimpset ctxt)));
+fun clasimp_meth' tac prems ctxt = Method.METHOD (fn facts =>
+  FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_clasimpset ctxt)));
 
-val clasimp_method = clasimp_args o clasimp_meth;
-val clasimp_method' = clasimp_args o clasimp_meth';
+val clasimp_method = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth;
+val clasimp_method' = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth';
 
 
 val setup =
diff -r 08b2d5c94b8a -r 1d2c099e98f7 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Tue Sep 21 17:26:42 1999 +0200
+++ b/src/Provers/classical.ML	Tue Sep 21 17:26:50 1999 +0200
@@ -162,8 +162,8 @@
   val xtra_intro_local: Proof.context attribute
   val delrule_local: Proof.context attribute
   val cla_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
-  val cla_meth: (claset -> tactic) -> Proof.context -> Proof.method
-  val cla_meth': (claset -> int -> tactic) -> Proof.context -> Proof.method
+  val cla_meth: (claset -> tactic) -> thm list -> Proof.context -> Proof.method
+  val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
   val cla_method: (claset -> tactic) -> Args.src -> Proof.context -> Proof.method
   val cla_method': (claset -> int -> tactic) -> Args.src -> Proof.context -> Proof.method
   val setup: (theory -> theory) list
@@ -347,7 +347,7 @@
 	  cs)
   else
   let val (safe0_rls, safep_rls) = (*0 subgoals vs 1 or more*)
-          partition (fn rl => nprems_of rl=0) [th]
+          partition Thm.no_prems [th]
       val nI = length safeIs + 1
       and nE = length safeEs
   in warn_dup th cs;
@@ -530,7 +530,7 @@
           (cs as CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, swrappers, uwrappers,
 		    safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair}) =
  if mem_thm (th, safeIs) then
-   let val (safe0_rls, safep_rls) = partition (fn rl => nprems_of rl=0) [th]
+   let val (safe0_rls, safep_rls) = partition Thm.no_prems [th]
    in CS{safe0_netpair = delete (safe0_rls, []) safe0_netpair,
 	 safep_netpair = delete (safep_rls, []) safep_netpair,
 	 safeIs	= rem_thm (safeIs,th),
@@ -1145,16 +1145,14 @@
   Args.$$$ introN >> K (I, safe_intro_local),
   Args.$$$ delN >> K (I, delrule_local)];
 
-val cla_args = Method.only_sectioned_args cla_modifiers;
-
-fun cla_meth tac ctxt = Method.METHOD (fn facts =>
-  ALLGOALS (Method.insert_tac facts) THEN tac (get_local_claset ctxt));
+fun cla_meth tac prems ctxt = Method.METHOD (fn facts =>
+  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_claset ctxt));
 
-fun cla_meth' tac ctxt = Method.METHOD (fn facts =>
-  FIRSTGOAL (Method.insert_tac facts THEN' tac (get_local_claset ctxt)));
+fun cla_meth' tac prems ctxt = Method.METHOD (fn facts =>
+  FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_claset ctxt)));
 
-val cla_method = cla_args o cla_meth;
-val cla_method' = cla_args o cla_meth';
+val cla_method = Method.bang_sectioned_args cla_modifiers o cla_meth;
+val cla_method' = Method.bang_sectioned_args cla_modifiers o cla_meth';