src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
changeset 43292 ff3d49e77359
parent 43290 07eb0ad9bb93
child 43306 03e6da81aee6
equal deleted inserted replaced
43291:9f33b4ec866c 43292:ff3d49e77359
    75 
    75 
    76 fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
    76 fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
    77              ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
    77              ({state, subgoal, subgoal_count, facts, ...} : prover_problem)
    78              (result as {outcome, used_facts, run_time_in_msecs, preplay,
    78              (result as {outcome, used_facts, run_time_in_msecs, preplay,
    79                          message, message_tail} : prover_result) =
    79                          message, message_tail} : prover_result) =
    80   if is_some outcome then
    80   if is_some outcome orelse null used_facts then
    81     result
    81     result
    82   else
    82   else
    83     let
    83     let
    84       val num_facts = length used_facts
    84       val num_facts = length used_facts
    85       val ((minimize, minimize_name), preplay) =
    85       val ((minimize, minimize_name), preplay) =