1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 20 08:44:24 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 20 08:44:24 2013 +0100
     1.3 @@ -295,7 +295,11 @@
     1.4              in
     1.5                (case Lazy.force preplay of
     1.6                   Played (reconstr as Metis _, timeout) =>
     1.7 -                 if can_min_fast_enough timeout then
     1.8 +                 if isar_proofs = SOME true then
     1.9 +                   (* Cheat: Assume the original prover is as fast as "metis"
    1.10 +                      for the goal it proved itself. *)
    1.11 +                   (can_min_fast_enough timeout, (name, params))
    1.12 +                 else if can_min_fast_enough timeout then
    1.13                     (true, extract_reconstructor params reconstr
    1.14                            ||> (fn override_params =>
    1.15                                    adjust_reconstructor_params override_params
    1.16 @@ -303,7 +307,7 @@
    1.17                   else
    1.18                     (prover_fast_enough (), (name, params))
    1.19                 | Played (SMT, timeout) =>
    1.20 -                 (* Cheat: assume the original prover is as fast as "smt" for
    1.21 +                 (* Cheat: Assume the original prover is as fast as "smt" for
    1.22                      the goal it proved itself *)
    1.23                   (can_min_fast_enough timeout, (name, params))
    1.24                 | _ => (prover_fast_enough (), (name, params)),