1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jun 08 16:20:18 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Jun 08 16:20:18 2011 +0200
     1.3 @@ -77,7 +77,7 @@
     1.4               ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
     1.5               (result as {outcome, used_facts, run_time_in_msecs, preplay,
     1.6                           message, message_tail} : prover_result) =
     1.7 -  if is_some outcome then
     1.8 +  if is_some outcome orelse null used_facts then
     1.9      result
    1.10    else
    1.11      let