# HG changeset patch
# User wenzelm
# Date 1376762056 -7200
# Node ID 6a3320758f0d161c107cff99f66638ef2ab5c891
# Parent  a0db255af8c52b95b60b47c9c0f061b247cdc8f1
always enable "minimize" to simplify interaction model;
override params more directly -- they are no longer echoed in minimize command;

diff -r a0db255af8c5 -r 6a3320758f0d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Aug 17 19:13:28 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Aug 17 19:54:16 2013 +0200
@@ -503,17 +503,16 @@
           val [provers_arg, timeout_arg, isar_proofs_arg] = args;
           val ctxt = Proof.context_of state
 
-          val {debug, verbose, overlord, isar_proofs, ...} = get_params Normal ctxt []
           val override_params =
-            ([("timeout", [timeout_arg]), ("blocking", ["true"])] @
-            (if Option.map Bool.toString isar_proofs <> SOME isar_proofs_arg
-             then [("isar_proofs", [isar_proofs_arg])] else []) @
-            (if debug then [("debug", ["false"])] else []) @
-            (if verbose then [("verbose", ["false"])] else []) @
-            (if overlord then [("overlord", ["false"])] else []) @
-            (if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]))
+            ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
+              [("timeout", [timeout_arg]),
+               ("isar_proofs", [isar_proofs_arg]),
+               ("blocking", ["true"]),
+               ("minimize", ["true"]),
+               ("debug", ["false"]),
+               ("verbose", ["false"]),
+               ("overlord", ["false"])])
             |> map (normalize_raw_param ctxt)
-
           val _ =
             run_sledgehammer (get_params Normal ctxt override_params) Normal (SOME output_result) 1
               no_fact_override (minimize_command override_params 1) state