--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Aug 17 14:13:18 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Aug 17 19:13:28 2013 +0200
@@ -502,9 +502,8 @@
let
val [provers_arg, timeout_arg, isar_proofs_arg] = args;
val ctxt = Proof.context_of state
- val mode = Normal_Result
- val {debug, verbose, overlord, isar_proofs, ...} = get_params mode ctxt []
+ 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
@@ -516,7 +515,7 @@
|> map (normalize_raw_param ctxt)
val _ =
- run_sledgehammer (get_params mode ctxt override_params) mode (SOME output_result) 1
+ run_sledgehammer (get_params Normal ctxt override_params) Normal (SOME output_result) 1
no_fact_override (minimize_command override_params 1) state
in () end
| NONE => error "Unknown proof context"));