# HG changeset patch # User blanchet # Date 1412079487 -7200 # Node ID ed380b9594b5c2d4bbb89bfdb2451d73213e3a54 # Parent 308f3c7dfb67ef651d5764045805ee65fb74c033 always minimize, to reinvoke the prover with nicer options and yield a nicer Isar proof (potentially -- cf. 'full_proof') diff -r 308f3c7dfb67 -r ed380b9594b5 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML --- 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