# HG changeset patch
# User blanchet
# Date 1361346264 -3600
# Node ID 89e9e945a005f426083192de0fd50a6f9dda5b4f
# Parent  2654b3965c8d4c5bca234f308ed5179772c815da
auto-minimizer should respect "isar_proofs = true"

diff -r 2654b3965c8d -r 89e9e945a005 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 20 08:44:24 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Feb 20 08:44:24 2013 +0100
@@ -295,7 +295,11 @@
             in
               (case Lazy.force preplay of
                  Played (reconstr as Metis _, timeout) =>
-                 if can_min_fast_enough timeout then
+                 if isar_proofs = SOME true then
+                   (* Cheat: Assume the original prover is as fast as "metis"
+                      for the goal it proved itself. *)
+                   (can_min_fast_enough timeout, (name, params))
+                 else if can_min_fast_enough timeout then
                    (true, extract_reconstructor params reconstr
                           ||> (fn override_params =>
                                   adjust_reconstructor_params override_params
@@ -303,7 +307,7 @@
                  else
                    (prover_fast_enough (), (name, params))
                | Played (SMT, timeout) =>
-                 (* Cheat: assume the original prover is as fast as "smt" for
+                 (* Cheat: Assume the original prover is as fast as "smt" for
                     the goal it proved itself *)
                  (can_min_fast_enough timeout, (name, params))
                | _ => (prover_fast_enough (), (name, params)),