# HG changeset patch
# User blanchet
# Date 1406280383 -7200
# Node ID 858c1a63967fe75cc1cef83345045792cff6ad5e
# Parent  6be7551476955ff2b4acca83429c265a0e71ceb7
don't lose 'minimize' flag before it reaches Isar proof text generation

diff -r 6be755147695 -r 858c1a63967f src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Jul 25 11:26:19 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Jul 25 11:26:23 2014 +0200
@@ -130,7 +130,7 @@
 
 fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
       type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
-      preplay_timeout, ...} : params)
+      minimize, preplay_timeout, ...} : params)
     silent (prover : prover) timeout i n state goal facts =
   let
     val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
@@ -144,7 +144,7 @@
        max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
        max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
        isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
-       slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout,
+       slice = false, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
        expect = ""}
     val problem =
       {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,