--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 13 10:29:49 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 13 11:34:56 2013 +0200
@@ -157,7 +157,7 @@
state |> Proof.map_context
(Config.put sledgehammer_result (quote name ^ ": " ^ message ()))
else
- ((if outcome_code = someN orelse mode = Normal then
+ ((if outcome_code = someN orelse mode = Normal orelse mode = Normal_Result then
quote name ^ ": " ^ message ()
else
"")
@@ -294,7 +294,7 @@
|> Par_List.map (fn f => ignore (f (unknownN, state)))
handle ERROR msg => (print ("Error: " ^ msg); error msg)
fun maybe f (accum as (outcome_code, _)) =
- accum |> (mode = Normal orelse outcome_code <> someN) ? f
+ accum |> (mode = Normal orelse mode = Normal_Result orelse outcome_code <> someN) ? f
in
(unknownN, state)
|> (if blocking then