only invoke metisFT if metis failed

--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Dec 10 11:58:26 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Thu Dec 10 18:10:59 2009 +0100
@@ -20,7 +20,8 @@
   type run_action = int -> run_args -> unit
   type action = init_action * run_action * done_action
   val catch : (int -> string) -> run_action -> run_action
-  val app_timeout : (int -> string) -> run_action -> run_action -> run_action
+  val catch_result : (int -> string) -> 'a -> (int -> run_args -> 'a) ->
+    int -> run_args -> 'a
   val register : action -> theory -> theory
   val step_hook : Toplevel.transition -> Toplevel.state -> Toplevel.state ->
     unit
@@ -70,21 +71,15 @@
 )
 
 
-fun app_with f g x = (g x; ())
-  handle (exn as Exn.Interrupt) => reraise exn | exn => (f exn; ())
-
 fun log_exn log tag id e = log (tag id ^ "exception:\n" ^ General.exnMessage e)
 
-fun catch tag f id (st as {log, ...}: run_args) =
-  app_with (log_exn log tag id) (f id) st
+fun catch tag f id (st as {log, ...}: run_args) = (f id st; ())
+  handle (exn as Exn.Interrupt) => reraise exn
+       | exn => (log_exn log tag id exn; ())
 
-fun app_timeout tag f g id (st as {log, ...}: run_args) =
-  let
-    val continue = (f id st; true)
-      handle (exn as Exn.Interrupt) => reraise exn
-           | (exn as TimeLimit.TimeOut) => (log_exn log tag id exn; false)
-           | _ => true
-  in if continue then g id st else () end
+fun catch_result tag d f id (st as {log, ...}: run_args) = f id st
+  handle (exn as Exn.Interrupt) => reraise exn
+       | exn => (log_exn log tag id exn; d)
 
 fun register (init, run, done) thy =
   let val id = length (Actions.get thy) + 1

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Dec 10 11:58:26 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Dec 10 18:10:59 2009 +0100
@@ -418,16 +418,19 @@
           change_data id (inc_metis_posns m pos);
           if name = "proof" then change_data id (inc_metis_proofs m) else ();
           "succeeded (" ^ string_of_int t ^ ")")
-    fun timed_metis thms = with_time (Mirabelle.cpu_time apply_metis thms)
-      handle TimeLimit.TimeOut => (change_data id (inc_metis_timeout m); "timeout")
-           | ERROR msg => "error: " ^ msg
+    fun timed_metis thms =
+      (with_time (Mirabelle.cpu_time apply_metis thms), true)
+      handle TimeLimit.TimeOut => (change_data id (inc_metis_timeout m);
+               ("timeout", false))
+           | ERROR msg => ("error: " ^ msg, false)
 
     val _ = log separator
     val _ = change_data id (inc_metis_calls m)
   in
     maps snd named_thms
     |> timed_metis
-    |> log o prefix (metis_tag id) 
+    |>> log o prefix (metis_tag id)
+    |> snd
   end
 
 fun sledgehammer_action args id (st as {pre, name, ...}: Mirabelle.run_args) =
@@ -442,13 +445,15 @@
     fun apply_metis m1 m2 =
       if metis_ft
       then
-        Mirabelle.app_timeout metis_tag
-          (run_metis false m1 name (these (!named_thms)))
-          (Mirabelle.catch metis_tag
-            (run_metis true m2 name (these (!named_thms)))) id st
+        if not (Mirabelle.catch_result metis_tag false
+            (run_metis false m1 name (these (!named_thms))) id st)
+        then
+          (Mirabelle.catch_result metis_tag false
+            (run_metis true m2 name (these (!named_thms))) id st; ())
+        else ()
       else
-        Mirabelle.catch metis_tag
-          (run_metis false m1 name (these (!named_thms))) id st
+        (Mirabelle.catch_result metis_tag false
+          (run_metis false m1 name (these (!named_thms))) id st; ())
   in 
     change_data id (set_mini minimize);
     Mirabelle.catch sh_tag (run_sledgehammer args named_thms) id st;