1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -256,7 +256,7 @@
     1.4    end
     1.5  
     1.6  fun maybe_minimize ctxt mode do_learn name
     1.7 -        (params as {debug, verbose, isar_proof, minimize, ...})
     1.8 +        (params as {verbose, isar_proof, minimize, ...})
     1.9          ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
    1.10          (result as {outcome, used_facts, run_time, preplay, message,
    1.11                      message_tail} : prover_result) =
    1.12 @@ -310,19 +310,8 @@
    1.13      in
    1.14        case used_facts of
    1.15          SOME used_facts =>
    1.16 -        (if debug andalso not (null used_facts) then
    1.17 -           tag_list 1 facts
    1.18 -           |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j))
    1.19 -           |> filter_used_facts used_facts
    1.20 -           |> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
    1.21 -           |> commas
    1.22 -           |> enclose ("Fact" ^ plural_s (length facts) ^ " in " ^ quote name ^
    1.23 -                       " proof (of " ^ string_of_int (length facts) ^ "): ") "."
    1.24 -           |> Output.urgent_message
    1.25 -         else
    1.26 -           ();
    1.27 -         {outcome = NONE, used_facts = used_facts, run_time = run_time,
    1.28 -          preplay = preplay, message = message, message_tail = message_tail})
    1.29 +        {outcome = NONE, used_facts = used_facts, run_time = run_time,
    1.30 +         preplay = preplay, message = message, message_tail = message_tail}
    1.31        | NONE => result
    1.32      end
    1.33