1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sat Dec 18 23:31:22 2010 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Sun Dec 19 00:13:25 2010 +0100
     1.3 @@ -30,10 +30,10 @@
     1.4  
     1.5  (* wrapper for calling external prover *)
     1.6  
     1.7 -fun string_for_failure ATP_Proof.Unprovable = "Unprovable."
     1.8 -  | string_for_failure ATP_Proof.TimedOut = "Timed out."
     1.9 -  | string_for_failure ATP_Proof.Interrupted = "Interrupted."
    1.10 -  | string_for_failure _ = "Error."
    1.11 +fun short_string_for_failure ATP_Proof.Unprovable = "Unprovable."
    1.12 +  | short_string_for_failure ATP_Proof.TimedOut = "Timed out."
    1.13 +  | short_string_for_failure ATP_Proof.Interrupted = "Interrupted."
    1.14 +  | short_string_for_failure _ = "Error."
    1.15  
    1.16  fun n_facts names =
    1.17    let val n = length names in
    1.18 @@ -47,11 +47,15 @@
    1.19  
    1.20  fun print silent f = if silent then () else Output.urgent_message (f ())
    1.21  
    1.22 -fun test_facts ({debug, overlord, provers, type_sys, isar_proof,
    1.23 +fun test_facts ({debug, verbose, overlord, provers, type_sys, isar_proof,
    1.24                   isar_shrink_factor, ...} : params) silent (prover : prover)
    1.25                 explicit_apply timeout i n state facts =
    1.26    let
    1.27 -    val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^ "...")
    1.28 +    val _ =
    1.29 +      print silent (fn () =>
    1.30 +          "Testing " ^ n_facts (map fst facts) ^
    1.31 +          (if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
    1.32 +          else "") ^ "...")
    1.33      val params =
    1.34        {debug = debug, verbose = false, overlord = overlord, blocking = true,
    1.35         provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
    1.36 @@ -66,12 +70,12 @@
    1.37         facts = facts, smt_head = NONE}
    1.38      val result as {outcome, used_facts, ...} = prover params (K "") problem
    1.39    in
    1.40 -    print silent
    1.41 -        (fn () => case outcome of
    1.42 -                    SOME failure => string_for_failure failure
    1.43 -                  | NONE =>
    1.44 -                    if length used_facts = length facts then "Found proof."
    1.45 -                    else "Found proof with " ^ n_facts used_facts ^ ".");
    1.46 +    print silent (fn () =>
    1.47 +        case outcome of
    1.48 +          SOME failure => short_string_for_failure failure
    1.49 +        | NONE =>
    1.50 +          if length used_facts = length facts then "Found proof."
    1.51 +          else "Found proof with " ^ n_facts used_facts ^ ".");
    1.52      result
    1.53    end
    1.54  
    1.55 @@ -123,7 +127,7 @@
    1.56  (* Give the external prover some slack. The ATP gets further slack because the
    1.57     Sledgehammer preprocessing time is included in the estimate below but isn't
    1.58     part of the timeout. *)
    1.59 -val fudge_msecs = 1000
    1.60 +val slack_msecs = 200
    1.61  
    1.62  fun minimize_facts prover_name (params as {timeout, ...}) silent i n state
    1.63                     facts =
    1.64 @@ -148,7 +152,7 @@
    1.65         let
    1.66           val time = Timer.checkRealTimer timer
    1.67           val new_timeout =
    1.68 -           Int.min (msecs, Time.toMilliseconds time + fudge_msecs)
    1.69 +           Int.min (msecs, Time.toMilliseconds time + slack_msecs)
    1.70             |> Time.fromMilliseconds
    1.71           val facts = filter_used_facts used_facts facts
    1.72           val (min_thms, {message, ...}) =