simplified data structure

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Dec 19 10:12:28 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Dec 19 10:15:12 2013 +0100
@@ -192,25 +192,21 @@
                    i n state goal preplay0 facts =
   let
     val ctxt = Proof.context_of state
-    val prover =
-      get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
+    val prover = get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
     fun test timeout = test_facts params silent prover timeout i n state goal
     val (chained, non_chained) = List.partition is_fact_chained facts
     (* Push chained facts to the back, so that they are less likely to be
        kicked out by the linear minimization algorithm. *)
     val facts = non_chained @ chained
   in
-    (print silent (fn () => "Sledgehammer minimizer: " ^
-                            quote prover_name ^ ".");
+    (print silent (fn () => "Sledgehammer minimizer: " ^ quote prover_name ^ ".");
      case test timeout facts of
        result as {outcome = NONE, used_facts, run_time, ...} =>
        let
          val facts = filter_used_facts true used_facts facts
          val min =
-           if length facts >= Config.get ctxt binary_min_facts then
-             binary_minimize
-           else
-             linear_minimize
+           if length facts >= Config.get ctxt binary_min_facts then binary_minimize
+           else linear_minimize
          val (min_facts, {preplay, message, message_tail, ...}) =
            min test (new_timeout timeout run_time) result facts
        in
@@ -221,10 +217,8 @@
                | n => "\n(including " ^ string_of_int n ^ " chained)") ^ ".");
          (if learn then do_learn (maps snd min_facts) else ());
          (SOME min_facts,
-          (if is_some preplay0 andalso length min_facts = length facts then
-             the preplay0
-           else
-             preplay,
+          (if is_some preplay0 andalso length min_facts = length facts then the preplay0
+           else preplay,
            message, message_tail))
        end
      | {outcome = SOME TimedOut, preplay, ...} =>
@@ -236,10 +230,8 @@
             string_of_int (10 + Time.toMilliseconds
                 (timeout |> the_default (seconds 60.0)) div 1000) ^
             "\").", ""))
-     | {preplay, message, ...} =>
-       (NONE, (preplay, prefix "Prover error: " o message, "")))
-    handle ERROR msg =>
-           (NONE, (Lazy.value (Play_Failed plain_metis), fn _ => "Error: " ^ msg, ""))
+     | {preplay, message, ...} => (NONE, (preplay, prefix "Prover error: " o message, "")))
+    handle ERROR msg => (NONE, (Lazy.value (Play_Failed plain_metis), fn _ => "Error: " ^ msg, ""))
   end
 
 fun adjust_reconstructor_params override_params

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Dec 19 10:12:28 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_print.ML	Thu Dec 19 10:15:12 2013 +0100
@@ -86,14 +86,11 @@
   let
     val (chained, extra) = split_used_facts used_facts
     val (failed, reconstr, ext_time) =
-      case preplay of
+      (case preplay of
         Played (reconstr, time) => (false, reconstr, (SOME (false, time)))
       | Play_Timed_Out (reconstr, time) =>
-        (false, reconstr,
-         (case time of
-           NONE => NONE
-         | SOME time => if time = Time.zeroTime then NONE else SOME (true, time)))
-      | Play_Failed reconstr => (true, reconstr, NONE)
+        (false, reconstr, if time = Time.zeroTime then NONE else SOME (true, time))
+      | Play_Failed reconstr => (true, reconstr, NONE))
     val try_line =
       ([], map fst extra)
       |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Dec 19 10:12:28 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Dec 19 10:15:12 2013 +0100
@@ -395,23 +395,21 @@
 fun filter_used_facts keep_chained used =
   filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
 
-fun play_one_line_proof mode debug verbose timeout pairs state i preferred
-                        reconstrs =
+fun play_one_line_proof mode debug verbose timeout pairs state i preferred reconstrs =
   let
     fun get_preferred reconstrs =
       if member (op =) reconstrs preferred then preferred
       else List.last reconstrs
   in
     if timeout = SOME Time.zeroTime then
-      Play_Timed_Out (get_preferred reconstrs, NONE)
+      Play_Timed_Out (get_preferred reconstrs, Time.zeroTime)
     else
       let
-        val _ =
-          if mode = Minimize then Output.urgent_message "Preplaying proof..."
-          else ()
+        val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
         val ths = pairs |> sort_wrt (fst o fst) |> map snd
         fun play [] [] = Play_Failed (get_preferred reconstrs)
-          | play timed_outs [] = Play_Timed_Out (get_preferred timed_outs, timeout)
+          | play timed_outs [] =
+            Play_Timed_Out (get_preferred timed_outs, timeout |> the_default Time.zeroTime (* wrong *))
           | play timed_out (reconstr :: reconstrs) =
             let
               val _ =

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Thu Dec 19 10:12:28 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Thu Dec 19 10:15:12 2013 +0100
@@ -15,7 +15,7 @@
 
   datatype play =
     Played of reconstructor * Time.time |
-    Play_Timed_Out of reconstructor * Time.time option |
+    Play_Timed_Out of reconstructor * Time.time |
     Play_Failed of reconstructor
 
   type minimize_command = string list -> string
@@ -35,7 +35,7 @@
 
 datatype play =
   Played of reconstructor * Time.time |
-  Play_Timed_Out of reconstructor * Time.time option |
+  Play_Timed_Out of reconstructor * Time.time |
   Play_Failed of reconstructor
 
 type minimize_command = string list -> string