# HG changeset patch
# User blanchet
# Date 1280336058 -7200
# Node ID 463177795c493a55fd60c2b2577de4e72a03e01c
# Parent  f31ddd5da4e39c3f677097df9cf86ca6b466e995
minor refactoring

diff -r f31ddd5da4e3 -r 463177795c49 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Jul 28 18:45:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Jul 28 18:54:18 2010 +0200
@@ -53,9 +53,9 @@
   val running_atps: unit -> unit
   val messages: int option -> unit
   val get_prover_fun : theory -> string -> prover
-  val start_prover_thread :
-    params -> int -> int -> relevance_override -> (string -> minimize_command)
-    -> Proof.state -> string -> unit
+  val run_sledgehammer :
+    params -> int -> relevance_override -> (string -> minimize_command)
+    -> Proof.state -> unit
   val setup : theory -> theory
 end;
 
@@ -845,7 +845,6 @@
 
 fun get_prover_fun thy name = prover_fun name (get_prover thy name)
 
-(* start prover thread *)
 fun start_prover_thread (params as {verbose, full_types, timeout, ...}) i n
                         relevance_override minimize_command proof_state name =
   let
@@ -871,6 +870,19 @@
             end)
   end
 
+fun run_sledgehammer {atps = [], ...} _ _ _ _ = error "No ATP is set."
+  | run_sledgehammer (params as {atps, ...}) i relevance_override
+                     minimize_command state =
+    case subgoal_count state of
+      0 => priority "No subgoal!"
+    | n =>
+      let
+        val _ = kill_atps ()
+        val _ = priority "Sledgehammering..."
+        val _ = app (start_prover_thread params i n relevance_override
+                                         minimize_command state) atps
+      in () end
+
 val setup =
   dest_dir_setup
   #> problem_prefix_setup
diff -r f31ddd5da4e3 -r 463177795c49 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 28 18:45:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 28 18:54:18 2010 +0200
@@ -188,22 +188,8 @@
 fun get_params thy = extract_params (default_raw_params thy)
 fun default_params thy = get_params thy o map (apsnd single)
 
-val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
-
 (* Sledgehammer the given subgoal *)
 
-fun run {atps = [], ...} _ _ _ _ = error "No ATP is set."
-  | run (params as {atps, ...}) i relevance_override minimize_command state =
-    case subgoal_count state of
-      0 => priority "No subgoal!"
-    | n =>
-      let
-        val _ = kill_atps ()
-        val _ = priority "Sledgehammering..."
-        val _ = app (start_prover_thread params i n relevance_override
-                                         minimize_command state) atps
-      in () end
-
 fun minimize override_params i refs state =
   let
     val thy = Proof.theory_of state
@@ -252,8 +238,8 @@
   in
     if subcommand = runN then
       let val i = the_default 1 opt_i in
-        run (get_params thy override_params) i relevance_override
-            (minimize_command override_params i) state
+        run_sledgehammer (get_params thy override_params) i relevance_override
+                         (minimize_command override_params i) state
       end
     else if subcommand = minimizeN then
       minimize (map (apfst minimizize_raw_param_name) override_params)
diff -r f31ddd5da4e3 -r 463177795c49 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Jul 28 18:45:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Wed Jul 28 18:54:18 2010 +0200
@@ -17,6 +17,7 @@
   val maybe_quote : string -> string
   val monomorphic_term : Type.tyenv -> term -> term
   val specialize_type : theory -> (string * typ) -> term -> term
+  val subgoal_count : Proof.state -> int
   val strip_subgoal : thm -> int -> (string * typ) list * term list * term
 end;
  
@@ -124,6 +125,8 @@
     | NONE => raise Type.TYPE_MATCH
   end
 
+val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
+
 fun strip_subgoal goal i =
   let
     val (t, frees) = Logic.goal_params (prop_of goal) i