changeset 58494 | ed380b9594b5 |
parent 58085 | ee65e9cfe284 |
child 58654 | 3e1cad27fc2f |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Tue Sep 30 14:01:33 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Tue Sep 30 14:18:07 2014 +0200 @@ -228,7 +228,7 @@ ({state, goal, subgoal, subgoal_count, ...} : prover_problem) (result as {outcome, used_facts, used_from, preferred_methss, run_time, message} : prover_result) = - if is_some outcome orelse null used_facts then + if is_some outcome then result else let