# HG changeset patch
# User paulson
# Date 1192544316 -7200
# Node ID f8712e98756acaebd75dcdc84713a6461cc2aa55
# Parent  3d0137a59dcb140c0c10d7bcb6c59a09859f11e1
added the "max_sledgehammers" option

diff -r 3d0137a59dcb -r f8712e98756a src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Tue Oct 16 14:11:35 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML	Tue Oct 16 16:18:36 2007 +0200
@@ -25,6 +25,7 @@
   val pass_mark    : real ref
   val convergence  : real ref
   val max_new      : int ref
+  val max_sledgehammers : int ref
   val follow_defs  : bool ref
   val add_all : unit -> unit
   val add_claset : unit -> unit
@@ -57,6 +58,8 @@
 val run_blacklist_filter = ref true;
 val time_limit = ref 60;
 val prover = ref Recon.E;
+val max_sledgehammers = ref 1;
+
 
 (*** relevance filter parameters ***)
 val run_relevance_filter = ref true;
@@ -734,7 +737,7 @@
   FIXME: does not cope with &&, and it isn't easy because one could have multiple
   subgoals, each involving &&.*)
 fun write_problem_files probfile (ctxt, chain_ths, th) =
-  let val goals = Thm.prems_of th
+  let val goals = Library.take (!max_sledgehammers, Thm.prems_of th)  (*raises no exception*)
       val _ = Output.debug (fn () => "number of subgoals = " ^ Int.toString (length goals))
       val thy = ProofContext.theory_of ctxt
       fun get_neg_subgoals [] _ = []
@@ -799,7 +802,7 @@
 
 (*writes out the current problems and calls ATPs*)
 fun isar_atp (ctxt, chain_ths, th) =
-  if Thm.no_prems th then ()
+  if Thm.no_prems th then warning "Nothing to prove"
   else
     let
       val _ = kill_last_watcher()
@@ -820,7 +823,7 @@
 
 val isar_atp_writeonly = PrintMode.setmp []
       (fn (ctxt, chain_ths, th) =>
-       if Thm.no_prems th then ()
+       if Thm.no_prems th then warning "Nothing to prove"
        else
          let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix
                             else prob_pathname