1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jun 08 08:47:43 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Jun 08 08:47:43 2011 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4  fun print silent f = if silent then () else Output.urgent_message (f ())
     1.5  
     1.6  fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
     1.7 -                 max_new_mono_instances, type_sys, explicit_apply, isar_proof,
     1.8 +                 max_new_mono_instances, type_sys, isar_proof,
     1.9                   isar_shrink_factor, preplay_timeout, ...} : params)
    1.10                 silent (prover : prover) timeout i n state facts =
    1.11    let
    1.12 @@ -59,7 +59,7 @@
    1.13      val {goal, ...} = Proof.goal state
    1.14      val params =
    1.15        {debug = debug, verbose = verbose, overlord = overlord, blocking = true,
    1.16 -       provers = provers, type_sys = type_sys, explicit_apply = explicit_apply,
    1.17 +       provers = provers, type_sys = type_sys,
    1.18         relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
    1.19         max_mono_iters = max_mono_iters,
    1.20         max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
    1.21 @@ -73,16 +73,18 @@
    1.22      val result as {outcome, used_facts, run_time_in_msecs, ...} =
    1.23        prover params (K (K "")) problem
    1.24    in
    1.25 -    print silent (fn () =>
    1.26 -        case outcome of
    1.27 -          SOME failure => string_for_failure failure
    1.28 -        | NONE => "Found proof" ^
    1.29 -                  (if length used_facts = length facts then ""
    1.30 -                   else " with " ^ n_facts used_facts) ^
    1.31 -                  (case run_time_in_msecs of
    1.32 -                     SOME ms =>
    1.33 -                     " (" ^ string_from_time (Time.fromMilliseconds ms) ^ ")"
    1.34 -                   | NONE => "") ^ ".");
    1.35 +    print silent
    1.36 +          (fn () =>
    1.37 +              case outcome of
    1.38 +                SOME failure => string_for_failure failure
    1.39 +              | NONE =>
    1.40 +                "Found proof" ^
    1.41 +                 (if length used_facts = length facts then ""
    1.42 +                  else " with " ^ n_facts used_facts) ^
    1.43 +                 (case run_time_in_msecs of
    1.44 +                    SOME ms =>
    1.45 +                    " (" ^ string_from_time (Time.fromMilliseconds ms) ^ ")"
    1.46 +                  | NONE => "") ^ ".");
    1.47      result
    1.48    end
    1.49