# 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