--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Fri Jul 20 22:19:46 2012 +0200
@@ -256,7 +256,7 @@
end
fun maybe_minimize ctxt mode do_learn name
- (params as {debug, verbose, isar_proof, minimize, ...})
+ (params as {verbose, isar_proof, minimize, ...})
({state, subgoal, subgoal_count, facts, ...} : prover_problem)
(result as {outcome, used_facts, run_time, preplay, message,
message_tail} : prover_result) =
@@ -310,19 +310,8 @@
in
case used_facts of
SOME used_facts =>
- (if debug andalso not (null used_facts) then
- tag_list 1 facts
- |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j))
- |> filter_used_facts used_facts
- |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
- |> commas
- |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
- " proof (of " ^ string_of_int (length facts) ^ "): ") "."
- |> Output.urgent_message
- else
- ();
- {outcome = NONE, used_facts = used_facts, run_time = run_time,
- preplay = preplay, message = message, message_tail = message_tail})
+ {outcome = NONE, used_facts = used_facts, run_time = run_time,
+ preplay = preplay, message = message, message_tail = message_tail}
| NONE => result
end