1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri May 27 10:30:08 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Fri May 27 10:30:08 2011 +0200
     1.3 @@ -11,14 +11,23 @@
     1.4    type 'a proof = 'a ATP_Proof.proof
     1.5    type locality = Sledgehammer_Filter.locality
     1.6    type type_system = Sledgehammer_ATP_Translate.type_system
     1.7 +
     1.8 +  datatype reconstructor =
     1.9 +    Metis |
    1.10 +    MetisFT |
    1.11 +    SMT of string
    1.12 +
    1.13 +  datatype preplay =
    1.14 +    Preplayed of reconstructor * Time.time |
    1.15 +    Trust_Playable of reconstructor * Time.time option|
    1.16 +    Preplay_Failed
    1.17 +
    1.18    type minimize_command = string list -> string
    1.19 -  type metis_params =
    1.20 -    string * minimize_command * type_system * string proof * int
    1.21 -    * (string * locality) list vector * int list * thm * int
    1.22 +  type one_line_params =
    1.23 +    preplay * string * (string * locality) list * minimize_command * thm * int
    1.24    type isar_params =
    1.25 -    bool * int * string Symtab.table * int list list * int Symtab.table
    1.26 -  type text_result = string * (string * locality) list
    1.27 -
    1.28 +    bool * bool * int * type_system * string Symtab.table * int list list
    1.29 +    * int * (string * locality) list vector * int Symtab.table * string proof
    1.30    val repair_conjecture_shape_and_fact_names :
    1.31      type_system -> string -> int list list -> int
    1.32      -> (string * locality) list vector -> int list
    1.33 @@ -28,19 +37,22 @@
    1.34      -> string proof -> (string * locality) list
    1.35    val used_facts_in_unsound_atp_proof :
    1.36      Proof.context -> type_system -> int list list -> int
    1.37 -    -> (string * locality) list vector -> string proof -> string list option
    1.38 +    -> (string * locality) list vector -> 'a proof -> string list option
    1.39 +  val uses_typed_helpers : int list -> 'a proof -> bool
    1.40 +  val reconstructor_name : reconstructor -> string
    1.41 +  val reconstructor_settings : reconstructor -> string
    1.42    val apply_on_subgoal : string -> int -> int -> string
    1.43    val command_call : string -> string list -> string
    1.44 -  val try_command_line : string -> string -> string
    1.45 +  val try_command_line : string -> (bool * Time.time) option -> string -> string
    1.46    val minimize_line : ('a list -> string) -> 'a list -> string
    1.47    val split_used_facts :
    1.48      (string * locality) list
    1.49      -> (string * locality) list * (string * locality) list
    1.50 -  val metis_proof_text : Proof.context -> metis_params -> text_result
    1.51 +  val one_line_proof_text : one_line_params -> string
    1.52    val isar_proof_text :
    1.53 -    Proof.context -> isar_params -> metis_params -> text_result
    1.54 +    Proof.context -> isar_params -> one_line_params -> string
    1.55    val proof_text :
    1.56 -    Proof.context -> bool -> isar_params -> metis_params -> text_result
    1.57 +    Proof.context -> bool -> isar_params -> one_line_params -> string
    1.58  end;
    1.59  
    1.60  structure Sledgehammer_ATP_Reconstruct : SLEDGEHAMMER_ATP_RECONSTRUCT =
    1.61 @@ -53,13 +65,22 @@
    1.62  open Sledgehammer_Filter
    1.63  open Sledgehammer_ATP_Translate
    1.64  
    1.65 +datatype reconstructor =
    1.66 +  Metis |
    1.67 +  MetisFT |
    1.68 +  SMT of string
    1.69 +
    1.70 +datatype preplay =
    1.71 +  Preplayed of reconstructor * Time.time |
    1.72 +  Trust_Playable of reconstructor * Time.time option |
    1.73 +  Preplay_Failed
    1.74 +
    1.75  type minimize_command = string list -> string
    1.76 -type metis_params =
    1.77 -  string * minimize_command * type_system * string proof * int
    1.78 -  * (string * locality) list vector * int list * thm * int
    1.79 +type one_line_params =
    1.80 +  preplay * string * (string * locality) list * minimize_command * thm * int
    1.81  type isar_params =
    1.82 -  bool * int * string Symtab.table * int list list * int Symtab.table
    1.83 -type text_result = string * (string * locality) list
    1.84 +  bool * bool * int * type_system * string Symtab.table * int list list * int
    1.85 +  * (string * locality) list vector * int Symtab.table * string proof
    1.86  
    1.87  fun is_head_digit s = Char.isDigit (String.sub (s, 0))
    1.88  val scan_integer = Scan.many1 is_head_digit >> (the o Int.fromString o implode)
    1.89 @@ -223,10 +244,25 @@
    1.90        NONE
    1.91    end
    1.92  
    1.93 +fun uses_typed_helpers typed_helpers =
    1.94 +  exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name
    1.95 +           | _ => false)
    1.96 +
    1.97 +
    1.98  (** Soft-core proof reconstruction: Metis one-liner **)
    1.99  
   1.100 +fun reconstructor_name Metis = "metis"
   1.101 +  | reconstructor_name MetisFT = "metisFT"
   1.102 +  | reconstructor_name (SMT _) = "smt"
   1.103 +
   1.104 +fun reconstructor_settings (SMT settings) = settings
   1.105 +  | reconstructor_settings _ = ""
   1.106 +
   1.107  fun string_for_label (s, num) = s ^ string_of_int num
   1.108  
   1.109 +fun show_time NONE = ""
   1.110 +  | show_time (SOME ext_time) = " ~ " ^ string_from_ext_time ext_time
   1.111 +
   1.112  fun set_settings "" = ""
   1.113    | set_settings settings = "using [[" ^ settings ^ "]] "
   1.114  fun apply_on_subgoal settings _ 1 = set_settings settings ^ "by "
   1.115 @@ -235,15 +271,15 @@
   1.116      "prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal settings 1 n
   1.117  fun command_call name [] = name
   1.118    | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
   1.119 -fun try_command_line banner command =
   1.120 -  banner ^ ": " ^ Markup.markup Markup.sendback command ^ "."
   1.121 +fun try_command_line banner time command =
   1.122 +  banner ^ ": " ^ Markup.markup Markup.sendback command ^ show_time time ^ "."
   1.123  fun using_labels [] = ""
   1.124    | using_labels ls =
   1.125      "using " ^ space_implode " " (map string_for_label ls) ^ " "
   1.126 -fun metis_name full_types = if full_types then "metisFT" else "metis"
   1.127 -fun metis_call full_types ss = command_call (metis_name full_types) ss
   1.128 -fun metis_command full_types i n (ls, ss) =
   1.129 -  using_labels ls ^ apply_on_subgoal "" i n ^ metis_call full_types ss
   1.130 +fun reconstructor_command reconstructor i n (ls, ss) =
   1.131 +  using_labels ls ^
   1.132 +  apply_on_subgoal (reconstructor_settings reconstructor) i n ^
   1.133 +  command_call (reconstructor_name reconstructor) ss
   1.134  fun minimize_line _ [] = ""
   1.135    | minimize_line minimize_command ss =
   1.136      case minimize_command ss of
   1.137 @@ -254,24 +290,28 @@
   1.138    List.partition (curry (op =) Chained o snd)
   1.139    #> pairself (sort_distinct (string_ord o pairself fst))
   1.140  
   1.141 -fun uses_typed_helpers typed_helpers =
   1.142 -  exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name
   1.143 -           | _ => false)
   1.144 -
   1.145 -fun metis_proof_text ctxt (banner, minimize_command, type_sys, atp_proof,
   1.146 -                           facts_offset, fact_names, typed_helpers, goal, i) =
   1.147 +fun one_line_proof_text (preplay, banner, used_facts, minimize_command,
   1.148 +                         goal, i) =
   1.149    let
   1.150 -    val (chained, extra) =
   1.151 -      atp_proof |> used_facts_in_atp_proof ctxt type_sys facts_offset fact_names
   1.152 -                |> split_used_facts
   1.153 -    val full_types = uses_typed_helpers typed_helpers atp_proof
   1.154 +    val (chained, extra) = split_used_facts used_facts
   1.155 +    val (reconstructor, ext_time) =
   1.156 +      case preplay of
   1.157 +        Preplayed (reconstructor, time) =>
   1.158 +        (SOME reconstructor, (SOME (false, time)))
   1.159 +      | Trust_Playable (reconstructor, time) =>
   1.160 +        (SOME reconstructor,
   1.161 +         case time of
   1.162 +           NONE => NONE
   1.163 +         | SOME time =>
   1.164 +           if time = Time.zeroTime then NONE else SOME (true, time))
   1.165 +      | Preplay_Failed => (NONE, NONE)
   1.166      val n = Logic.count_prems (prop_of goal)
   1.167 -    val metis = metis_command full_types i n ([], map fst extra)
   1.168 -  in
   1.169 -    (try_command_line banner metis ^
   1.170 -     minimize_line minimize_command (map fst (extra @ chained)),
   1.171 -     extra @ chained)
   1.172 -  end
   1.173 +    val try_line =
   1.174 +      case reconstructor of
   1.175 +        SOME r => reconstructor_command r i n ([], map fst extra)
   1.176 +                  |> try_command_line banner ext_time
   1.177 +      | NONE => "Proof reconstruction failed."
   1.178 +  in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
   1.179  
   1.180  (** Hard-core proof reconstruction: structured Isar proofs **)
   1.181  
   1.182 @@ -702,8 +742,8 @@
   1.183        s
   1.184  
   1.185  fun isar_proof_from_atp_proof pool ctxt type_sys tfrees isar_shrink_factor
   1.186 -        atp_proof conjecture_shape facts_offset fact_names sym_tab params
   1.187 -        frees =
   1.188 +        conjecture_shape facts_offset fact_names sym_tab params frees
   1.189 +        atp_proof =
   1.190    let
   1.191      val lines =
   1.192        atp_proof
   1.193 @@ -976,10 +1016,11 @@
   1.194         else
   1.195           if member (op =) qs Show then "show" else "have")
   1.196      val do_term = maybe_quote o fix_print_mode (Syntax.string_of_term ctxt)
   1.197 +    val reconstructor = if full_types then MetisFT else Metis
   1.198      fun do_facts (ls, ss) =
   1.199 -      metis_command full_types 1 1
   1.200 -                    (ls |> sort_distinct (prod_ord string_ord int_ord),
   1.201 -                     ss |> sort_distinct string_ord)
   1.202 +      reconstructor_command reconstructor 1 1
   1.203 +          (ls |> sort_distinct (prod_ord string_ord int_ord),
   1.204 +           ss |> sort_distinct string_ord)
   1.205      and do_step ind (Fix xs) =
   1.206          do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n"
   1.207        | do_step ind (Let (t1, t2)) =
   1.208 @@ -1012,20 +1053,20 @@
   1.209    in do_proof end
   1.210  
   1.211  fun isar_proof_text ctxt
   1.212 -        (debug, isar_shrink_factor, pool, conjecture_shape, sym_tab)
   1.213 -        (metis_params as (_, _, type_sys, atp_proof, facts_offset, fact_names,
   1.214 -                          typed_helpers, goal, i)) =
   1.215 +        (debug, full_types, isar_shrink_factor, type_sys, pool,
   1.216 +         conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof)
   1.217 +        (one_line_params as (_, _, _, _, goal, i)) =
   1.218    let
   1.219      val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal i
   1.220      val frees = fold Term.add_frees (concl_t :: hyp_ts) []
   1.221      val tfrees = fold Term.add_tfrees (concl_t :: hyp_ts) []
   1.222 -    val full_types = uses_typed_helpers typed_helpers atp_proof
   1.223      val n = Logic.count_prems (prop_of goal)
   1.224 -    val (one_line_proof, lemma_names) = metis_proof_text ctxt metis_params
   1.225 +    val one_line_proof = one_line_proof_text one_line_params
   1.226      fun isar_proof_for () =
   1.227 -      case isar_proof_from_atp_proof pool ctxt type_sys tfrees
   1.228 -               isar_shrink_factor atp_proof conjecture_shape facts_offset
   1.229 -               fact_names sym_tab params frees
   1.230 +      case atp_proof
   1.231 +           |> isar_proof_from_atp_proof pool ctxt type_sys tfrees
   1.232 +                  isar_shrink_factor conjecture_shape facts_offset
   1.233 +                  fact_names sym_tab params frees
   1.234             |> redirect_proof hyp_ts concl_t
   1.235             |> kill_duplicate_assumptions_in_proof
   1.236             |> then_chain_proof
   1.237 @@ -1040,9 +1081,13 @@
   1.238        else
   1.239          try isar_proof_for ()
   1.240          |> the_default "\nWarning: The Isar proof construction failed."
   1.241 -  in (one_line_proof ^ isar_proof, lemma_names) end
   1.242 +  in one_line_proof ^ isar_proof end
   1.243  
   1.244 -fun proof_text ctxt isar_proof isar_params =
   1.245 -  if isar_proof then isar_proof_text ctxt isar_params else metis_proof_text ctxt
   1.246 +fun proof_text ctxt isar_proof isar_params
   1.247 +               (one_line_params as (preplay, _, _, _, _, _)) =
   1.248 +  (if isar_proof orelse preplay = Preplay_Failed then
   1.249 +     isar_proof_text ctxt isar_params
   1.250 +   else
   1.251 +     one_line_proof_text) one_line_params
   1.252  
   1.253  end;

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri May 27 10:30:08 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri May 27 10:30:08 2011 +0200
     2.3 @@ -11,7 +11,6 @@
     2.4    type params = Sledgehammer_Provers.params
     2.5  
     2.6    val binary_min_facts : int Config.T
     2.7 -  val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list
     2.8    val minimize_facts :
     2.9      string -> params -> bool option -> bool -> int -> int -> Proof.state
    2.10      -> ((string * locality) * thm list) list
    2.11 @@ -97,8 +96,6 @@
    2.12    Attrib.setup_config_int @{binding sledgehammer_minimize_binary_min_facts}
    2.13                            (K 20)
    2.14  
    2.15 -fun filter_used_facts used = filter (member (op =) used o fst)
    2.16 -
    2.17  fun sublinear_minimize _ [] p = p
    2.18    | sublinear_minimize test (x :: xs) (seen, result) =
    2.19      case test (xs @ seen) of
    2.20 @@ -204,7 +201,7 @@
    2.21             | prover :: _ =>
    2.22               (kill_provers ();
    2.23                minimize_facts prover params NONE false i n state facts
    2.24 -              |> #2 |> Output.urgent_message)
    2.25 +              |> snd |> Output.urgent_message)
    2.26    end
    2.27  
    2.28  end;

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:08 2011 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri May 27 10:30:08 2011 +0200
     3.3 @@ -99,6 +99,7 @@
     3.4    val kill_provers : unit -> unit
     3.5    val running_provers : unit -> unit
     3.6    val messages : int option -> unit
     3.7 +  val filter_used_facts : ''a list -> (''a * 'b) list -> (''a * 'b) list
     3.8    val get_prover : Proof.context -> mode -> string -> prover
     3.9  end;
    3.10  
    3.11 @@ -306,6 +307,7 @@
    3.12  
    3.13  type prover = params -> minimize_command -> prover_problem -> prover_result
    3.14  
    3.15 +
    3.16  (* configuration attributes *)
    3.17  
    3.18  val dest_dir =
    3.19 @@ -318,20 +320,6 @@
    3.20  val measure_run_time =
    3.21    Attrib.setup_config_bool @{binding sledgehammer_measure_run_time} (K false)
    3.22  
    3.23 -fun with_path cleanup after f path =
    3.24 -  Exn.capture f path
    3.25 -  |> tap (fn _ => cleanup path)
    3.26 -  |> Exn.release
    3.27 -  |> tap (after path)
    3.28 -
    3.29 -fun proof_banner mode blocking name =
    3.30 -  case mode of
    3.31 -    Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
    3.32 -  | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
    3.33 -  | Normal => if blocking then quote name ^ " found a proof"
    3.34 -              else "Try this"
    3.35 -  | Minimize => "Try this"
    3.36 -
    3.37  val smt_triggers =
    3.38    Attrib.setup_config_bool @{binding sledgehammer_smt_triggers} (K true)
    3.39  val smt_weights =
    3.40 @@ -379,6 +367,41 @@
    3.41  fun overlord_file_location_for_prover prover =
    3.42    (getenv "ISABELLE_HOME_USER", "prob_" ^ prover)
    3.43  
    3.44 +fun with_path cleanup after f path =
    3.45 +  Exn.capture f path
    3.46 +  |> tap (fn _ => cleanup path)
    3.47 +  |> Exn.release
    3.48 +  |> tap (after path)
    3.49 +
    3.50 +fun proof_banner mode blocking name =
    3.51 +  case mode of
    3.52 +    Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
    3.53 +  | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
    3.54 +  | Normal => if blocking then quote name ^ " found a proof"
    3.55 +              else "Try this"
    3.56 +  | Minimize => "Try this"
    3.57 +
    3.58 +(* based on "Mirabelle.can_apply" and generalized *)
    3.59 +fun try_apply timeout tac state i =
    3.60 +  let
    3.61 +    val {context = ctxt, facts, goal} = Proof.goal state
    3.62 +    val full_tac = Method.insert_tac facts i THEN tac ctxt i
    3.63 +  in try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal end
    3.64 +
    3.65 +fun try_metis debug timeout ths =
    3.66 +  try_apply timeout (Config.put Metis_Tactics.verbose debug
    3.67 +                     #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths))
    3.68 +
    3.69 +fun filter_used_facts used = filter (member (op =) used o fst)
    3.70 +
    3.71 +fun preplay_one_line_proof debug reconstructor_guess timeout ths state i =
    3.72 +  let val timer = Timer.startRealTimer () in
    3.73 +    case try_metis debug timeout ths state i of
    3.74 +      SOME (SOME _) => Preplayed (Metis, Timer.checkRealTimer timer)
    3.75 +    | SOME NONE => Preplay_Failed
    3.76 +    | NONE => Trust_Playable (reconstructor_guess, SOME timeout)
    3.77 +  end
    3.78 +
    3.79  
    3.80  (* generic TPTP-based ATPs *)
    3.81  
    3.82 @@ -485,7 +508,7 @@
    3.83            conj_sym_kind, prem_kind, formats, best_slices, ...} : atp_config)
    3.84          ({debug, verbose, overlord, blocking, type_sys, max_relevant,
    3.85            max_mono_iters, max_new_mono_instances, explicit_apply, isar_proof,
    3.86 -          isar_shrink_factor, slicing, timeout, ...} : params)
    3.87 +          isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
    3.88          minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =
    3.89    let
    3.90      val thy = Proof.theory_of state
    3.91 @@ -708,7 +731,7 @@
    3.92          extract_important_message output
    3.93        else
    3.94          ""
    3.95 -    fun append_to_message message =
    3.96 +    fun complete_message message =
    3.97        message ^
    3.98        (if verbose then
    3.99           "\nATP real CPU time: " ^
   3.100 @@ -719,21 +742,34 @@
   3.101           "\n\nImportant message from Dr. Geoff Sutcliffe:\n" ^ important_message
   3.102         else
   3.103           "")
   3.104 -    val isar_params =
   3.105 -      (debug, isar_shrink_factor, pool, conjecture_shape, sym_tab)
   3.106 -    val metis_params =
   3.107 -      (proof_banner mode blocking name, minimize_command, type_sys, atp_proof,
   3.108 -       facts_offset, fact_names, typed_helpers, goal, subgoal)
   3.109      val (outcome, (message, used_facts)) =
   3.110        case outcome of
   3.111          NONE =>
   3.112 -        (NONE, proof_text ctxt isar_proof isar_params metis_params
   3.113 -               |>> append_to_message)
   3.114 -      | SOME failure =>
   3.115 -        if failure = ProofMissing orelse failure = ProofIncomplete then
   3.116 -          (NONE, metis_proof_text ctxt metis_params |>> append_to_message)
   3.117 -        else
   3.118 -          (outcome, (string_for_failure failure, []))
   3.119 +        let
   3.120 +          val used_facts =
   3.121 +            used_facts_in_atp_proof ctxt type_sys facts_offset fact_names
   3.122 +                                    atp_proof
   3.123 +          val reconstructor_guess =
   3.124 +            if uses_typed_helpers typed_helpers atp_proof then MetisFT
   3.125 +            else Metis
   3.126 +          val ths = facts |> map untranslated_fact
   3.127 +                          |> filter_used_facts used_facts
   3.128 +                          |> map snd
   3.129 +          val preplay =
   3.130 +            preplay_one_line_proof debug reconstructor_guess preplay_timeout ths
   3.131 +                                   state subgoal
   3.132 +          val full_types = uses_typed_helpers typed_helpers atp_proof
   3.133 +          val isar_params =
   3.134 +            (debug, full_types, isar_shrink_factor, type_sys, pool,
   3.135 +             conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof)
   3.136 +          val one_line_params =
   3.137 +            (preplay, proof_banner mode blocking name, used_facts,
   3.138 +             minimize_command, goal, subgoal)
   3.139 +        in
   3.140 +          (NONE, (proof_text ctxt isar_proof isar_params one_line_params
   3.141 +                  |> complete_message, used_facts))
   3.142 +        end
   3.143 +      | SOME failure => (outcome, (string_for_failure failure, []))
   3.144    in
   3.145      {outcome = outcome, message = message, used_facts = used_facts,
   3.146       run_time_in_msecs = msecs}
   3.147 @@ -877,30 +913,6 @@
   3.148        end
   3.149    in do_slice timeout 1 NONE Time.zeroTime end
   3.150  
   3.151 -(* based on "Mirabelle.can_apply" and generalized *)
   3.152 -fun try_apply timeout tac state i =
   3.153 -  let
   3.154 -    val {context = ctxt, facts, goal} = Proof.goal state
   3.155 -    val full_tac = Method.insert_tac facts i THEN tac ctxt i
   3.156 -  in try (TimeLimit.timeLimit timeout (Seq.pull o full_tac)) goal end
   3.157 -
   3.158 -fun try_metis debug timeout ths =
   3.159 -  try_apply timeout (Config.put Metis_Tactics.verbose debug
   3.160 -                     #> (fn ctxt => Metis_Tactics.metis_tac ctxt ths))
   3.161 -
   3.162 -datatype metis_try =
   3.163 -  Preplayed of string * Time.time |
   3.164 -  Preplay_Timed_Out |
   3.165 -  Preplay_Failed
   3.166 -
   3.167 -fun preplay debug timeout ths state i =
   3.168 -  let val timer = Timer.startRealTimer () in
   3.169 -    case try_metis debug timeout ths state i of
   3.170 -      SOME (SOME _) => Preplayed ("metis", Timer.checkRealTimer timer)
   3.171 -    | SOME NONE => Preplay_Failed
   3.172 -    | NONE => Preplay_Timed_Out
   3.173 -  end
   3.174 -
   3.175  fun run_smt_solver mode name
   3.176          (params as {debug, verbose, blocking, preplay_timeout, ...})
   3.177          minimize_command
   3.178 @@ -920,14 +932,15 @@
   3.179          NONE =>
   3.180          let
   3.181            val (settings, method, time) =
   3.182 -            case preplay debug preplay_timeout (map snd used_facts) state
   3.183 -                         subgoal of
   3.184 -              Preplayed (method, time) => (method, "", SOME time)
   3.185 +            case preplay_one_line_proof debug Metis preplay_timeout
   3.186 +                    (map snd used_facts) state subgoal of
   3.187 +              Preplayed (method, time) =>
   3.188 +              ("", reconstructor_name method, SOME (false, time))
   3.189              | _ => (if name = SMT_Solver.solver_name_of ctxt then ""
   3.190                      else "smt_solver = " ^ maybe_quote name,
   3.191                      "smt", NONE)
   3.192          in
   3.193 -          try_command_line (proof_banner mode blocking name)
   3.194 +          try_command_line (proof_banner mode blocking name) time
   3.195                (apply_on_subgoal settings subgoal subgoal_count ^
   3.196                 command_call method (map fst other_lemmas)) ^
   3.197            minimize_line minimize_command

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri May 27 10:30:08 2011 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri May 27 10:30:08 2011 +0200
     4.3 @@ -11,6 +11,7 @@
     4.4    val simplify_spaces : string -> string
     4.5    val parse_bool_option : bool -> string -> string -> bool option
     4.6    val parse_time_option : string -> string -> Time.time option
     4.7 +  val string_from_ext_time : bool * Time.time -> string
     4.8    val string_from_time : Time.time -> string
     4.9    val nat_subscript : int -> string
    4.10    val unyxml : string -> string
    4.11 @@ -67,8 +68,14 @@
    4.12          SOME (seconds (the secs))
    4.13      end
    4.14  
    4.15 -fun string_from_time t =
    4.16 -  string_of_real (0.01 * Real.fromInt (Time.toMilliseconds t div 10)) ^ " s"
    4.17 +fun string_from_ext_time (plus, time) =
    4.18 +  let val ms = Time.toMilliseconds time in
    4.19 +    if plus then signed_string_of_int ((ms + 999) div 1000) ^ "+ s"
    4.20 +    else if ms < 1000 then signed_string_of_int ms ^ " ms"
    4.21 +    else string_of_real (0.01 * Real.fromInt (ms div 10)) ^ " s"
    4.22 +  end
    4.23 +
    4.24 +val string_from_time = string_from_ext_time o pair false
    4.25  
    4.26  val subscript = implode o map (prefix "\<^isub>") o raw_explode  (* FIXME Symbol.explode (?) *)
    4.27  fun nat_subscript n =