src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
changeset 58494 ed380b9594b5
parent 58085 ee65e9cfe284
child 58654 3e1cad27fc2f
equal deleted inserted replaced
58493:308f3c7dfb67 58494:ed380b9594b5
   226 
   226 
   227 fun maybe_minimize mode do_learn name (params as {verbose, minimize, ...})
   227 fun maybe_minimize mode do_learn name (params as {verbose, minimize, ...})
   228     ({state, goal, subgoal, subgoal_count, ...} : prover_problem)
   228     ({state, goal, subgoal, subgoal_count, ...} : prover_problem)
   229     (result as {outcome, used_facts, used_from, preferred_methss, run_time, message}
   229     (result as {outcome, used_facts, used_from, preferred_methss, run_time, message}
   230      : prover_result) =
   230      : prover_result) =
   231   if is_some outcome orelse null used_facts then
   231   if is_some outcome then
   232     result
   232     result
   233   else
   233   else
   234     let
   234     let
   235       val (used_facts, message) =
   235       val (used_facts, message) =
   236         if minimize then
   236         if minimize then