# HG changeset patch
# User blanchet
# Date 1292706939 -3600
# Node ID 3897af72c731864ed5c7a2348f7d8bbdeef1f5a0
# Parent  6a9306c427b93b5549ab93cf4437b7c7412e4d44
move relevance filter into hard timeout

diff -r 6a9306c427b9 -r 3897af72c731 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Dec 18 21:24:34 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Dec 18 22:15:39 2010 +0100
@@ -368,24 +368,25 @@
     val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
     val no_dangerous_types =
       Sledgehammer_ATP_Translate.types_dangerous_types type_sys
-    val facts =
-      Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
-          relevance_thresholds
-          (the_default default_max_relevant max_relevant) is_built_in_const
-          relevance_fudge relevance_override chained_ths hyp_ts concl_t
-    val problem =
-      {state = st', goal = goal, subgoal = i,
-       subgoal_count = Sledgehammer_Util.subgoal_count st,
-       facts = facts |> map Sledgehammer_Provers.Untranslated_Fact,
-       smt_head = NONE}
     val time_limit =
       (case hard_timeout of
         NONE => I
       | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
     val ({outcome, message, used_facts, run_time_in_msecs}
          : Sledgehammer_Provers.prover_result,
-        time_isa) = time_limit (Mirabelle.cpu_time
-                      (prover params (K ""))) problem
+        time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
+      let
+        val facts =
+          Sledgehammer_Filter.relevant_facts ctxt no_dangerous_types
+              relevance_thresholds
+              (the_default default_max_relevant max_relevant) is_built_in_const
+              relevance_fudge relevance_override chained_ths hyp_ts concl_t
+        val problem =
+          {state = st', goal = goal, subgoal = i,
+           subgoal_count = Sledgehammer_Util.subgoal_count st,
+           facts = facts |> map Sledgehammer_Provers.Untranslated_Fact,
+           smt_head = NONE}
+      in prover params (K "") problem end)) ()
       handle TimeLimit.TimeOut =>
              ({outcome = SOME ATP_Proof.TimedOut, message = "", used_facts = [],
                run_time_in_msecs = NONE}, ~1)