1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Jul 28 18:45:18 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Jul 28 18:54:18 2010 +0200
     1.3 @@ -53,9 +53,9 @@
     1.4    val running_atps: unit -> unit
     1.5    val messages: int option -> unit
     1.6    val get_prover_fun : theory -> string -> prover
     1.7 -  val start_prover_thread :
     1.8 -    params -> int -> int -> relevance_override -> (string -> minimize_command)
     1.9 -    -> Proof.state -> string -> unit
    1.10 +  val run_sledgehammer :
    1.11 +    params -> int -> relevance_override -> (string -> minimize_command)
    1.12 +    -> Proof.state -> unit
    1.13    val setup : theory -> theory
    1.14  end;
    1.15  
    1.16 @@ -845,7 +845,6 @@
    1.17  
    1.18  fun get_prover_fun thy name = prover_fun name (get_prover thy name)
    1.19  
    1.20 -(* start prover thread *)
    1.21  fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
    1.22                          relevance_override minimize_command proof_state name =
    1.23    let
    1.24 @@ -871,6 +870,19 @@
    1.25              end)
    1.26    end
    1.27  
    1.28 +fun run_sledgehammer {atps = [], ...} _ _ _ _ = error "No ATP is set."
    1.29 +  | run_sledgehammer (params as {atps, ...}) i relevance_override
    1.30 +                     minimize_command state =
    1.31 +    case subgoal_count state of
    1.32 +      0 => priority "No subgoal!"
    1.33 +    | n =>
    1.34 +      let
    1.35 +        val _ = kill_atps ()
    1.36 +        val _ = priority "Sledgehammering..."
    1.37 +        val _ = app (start_prover_thread params i n relevance_override
    1.38 +                                         minimize_command state) atps
    1.39 +      in () end
    1.40 +
    1.41  val setup =
    1.42    dest_dir_setup
    1.43    #> problem_prefix_setup

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 28 18:45:18 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 28 18:54:18 2010 +0200
     2.3 @@ -188,22 +188,8 @@
     2.4  fun get_params thy = extract_params (default_raw_params thy)
     2.5  fun default_params thy = get_params thy o map (apsnd single)
     2.6  
     2.7 -val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
     2.8 -
     2.9  (* Sledgehammer the given subgoal *)
    2.10  
    2.11 -fun run {atps = [], ...} _ _ _ _ = error "No ATP is set."
    2.12 -  | run (params as {atps, ...}) i relevance_override minimize_command state =
    2.13 -    case subgoal_count state of
    2.14 -      0 => priority "No subgoal!"
    2.15 -    | n =>
    2.16 -      let
    2.17 -        val _ = kill_atps ()
    2.18 -        val _ = priority "Sledgehammering..."
    2.19 -        val _ = app (start_prover_thread params i n relevance_override
    2.20 -                                         minimize_command state) atps
    2.21 -      in () end
    2.22 -
    2.23  fun minimize override_params i refs state =
    2.24    let
    2.25      val thy = Proof.theory_of state
    2.26 @@ -252,8 +238,8 @@
    2.27    in
    2.28      if subcommand = runN then
    2.29        let val i = the_default 1 opt_i in
    2.30 -        run (get_params thy override_params) i relevance_override
    2.31 -            (minimize_command override_params i) state
    2.32 +        run_sledgehammer (get_params thy override_params) i relevance_override
    2.33 +                         (minimize_command override_params i) state
    2.34        end
    2.35      else if subcommand = minimizeN then
    2.36        minimize (map (apfst minimizize_raw_param_name) override_params)

     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Jul 28 18:45:18 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Jul 28 18:54:18 2010 +0200
     3.3 @@ -17,6 +17,7 @@
     3.4    val maybe_quote : string -> string
     3.5    val monomorphic_term : Type.tyenv -> term -> term
     3.6    val specialize_type : theory -> (string * typ) -> term -> term
     3.7 +  val subgoal_count : Proof.state -> int
     3.8    val strip_subgoal : thm -> int -> (string * typ) list * term list * term
     3.9  end;
    3.10   
    3.11 @@ -124,6 +125,8 @@
    3.12      | NONE => raise Type.TYPE_MATCH
    3.13    end
    3.14  
    3.15 +val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
    3.16 +
    3.17  fun strip_subgoal goal i =
    3.18    let
    3.19      val (t, frees) = Logic.goal_params (prop_of goal) i