src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Jun 12 17:10:12 2014 +0200
@@ -129,8 +129,8 @@
 fun print silent f = if silent then () else Output.urgent_message (f ())
 
 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_isar, try0_isar,
-      smt_proofs, preplay_timeout, ...} : params)
+      type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
+      preplay_timeout, ...} : params)
     silent (prover : prover) timeout i n state goal facts =
   let
     val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
@@ -143,9 +143,9 @@
        uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
        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_isar = compress_isar, try0_isar = try0_isar,
-       smt_proofs = smt_proofs, slice = false, minimize = SOME false, timeout = timeout,
-       preplay_timeout = preplay_timeout, expect = ""}
+       isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
+       slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout,
+       expect = ""}
     val problem =
       {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
        factss = [("", facts)]}
@@ -288,8 +288,8 @@
 fun adjust_proof_method_params override_params
     ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans,
       uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters,
-      max_new_mono_instances, isar_proofs, compress_isar, try0_isar, smt_proofs, slice, minimize,
-      timeout, preplay_timeout, expect} : params) =
+      max_new_mono_instances, isar_proofs, compress, try0, smt_proofs, slice, minimize, timeout,
+      preplay_timeout, expect} : params) =
   let
     fun lookup_override name default_value =
       (case AList.lookup (op =) override_params name of
@@ -304,8 +304,8 @@
      uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
      max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
-     compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice,
-     minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+     compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize,
+     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   end
 
 fun maybe_minimize ctxt mode do_learn name (params as {verbose, isar_proofs, minimize, ...})