1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Jul 25 11:26:19 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Fri Jul 25 11:26:23 2014 +0200
     1.3 @@ -130,7 +130,7 @@
     1.4  
     1.5  fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
     1.6        type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
     1.7 -      preplay_timeout, ...} : params)
     1.8 +      minimize, preplay_timeout, ...} : params)
     1.9      silent (prover : prover) timeout i n state goal facts =
    1.10    let
    1.11      val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
    1.12 @@ -144,7 +144,7 @@
    1.13         max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
    1.14         max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
    1.15         isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
    1.16 -       slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout,
    1.17 +       slice = false, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
    1.18         expect = ""}
    1.19      val problem =
    1.20        {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,