src/HOL/Tools/Sledgehammer/sledgehammer.ML
changeset 57053 46000c075d07
parent 57037 c51132be8e16
child 57056 8b2283566f6e
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu May 22 03:29:35 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu May 22 03:29:35 2014 +0200
     1.3 @@ -54,15 +54,9 @@
     1.4         ordered_outcome_codes
     1.5    |> the_default unknownN
     1.6  
     1.7 -fun prover_description ctxt ({verbose, blocking, ...} : params) name num_facts i n goal =
     1.8 +fun prover_description verbose name num_facts =
     1.9    (quote name,
    1.10 -   (if verbose then
    1.11 -      " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts
    1.12 -    else
    1.13 -      "") ^
    1.14 -   " on " ^ (if n = 1 then "goal" else "subgoal " ^ string_of_int i) ^
    1.15 -   (if blocking then "."
    1.16 -    else "\n" ^ Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i))))
    1.17 +   if verbose then " with " ^ string_of_int num_facts ^ " fact" ^ plural_s num_facts else "")
    1.18  
    1.19  fun launch_prover (params as {debug, verbose, spy, blocking, max_facts, timeout, expect, ...}) mode
    1.20      output_result minimize_command only learn
    1.21 @@ -77,8 +71,6 @@
    1.22      val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
    1.23      val num_facts = length facts |> not only ? Integer.min max_facts
    1.24  
    1.25 -    fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal
    1.26 -
    1.27      val problem =
    1.28        {comment = comment, state = state, goal = goal, subgoal = subgoal,
    1.29         subgoal_count = subgoal_count,
    1.30 @@ -195,7 +187,8 @@
    1.31              |> List.app Output.urgent_message
    1.32        in (outcome_code, state) end
    1.33      else
    1.34 -      (Async_Manager.thread SledgehammerN birth_time death_time (desc ())
    1.35 +      (Async_Manager.thread SledgehammerN birth_time death_time
    1.36 +         (prover_description verbose name num_facts)
    1.37           ((fn (outcome_code, message) => (verbose orelse outcome_code = someN, message ())) o go);
    1.38         (unknownN, state))
    1.39    end