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

diff -r 463177795c49 -r f367847f5068 src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Wed Jul 28 18:54:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Wed Jul 28 19:01:07 2010 +0200
@@ -8,11 +8,8 @@
 signature SLEDGEHAMMER_FACT_MINIMIZER =
 sig
   type params = Sledgehammer.params
-  type prover_result = Sledgehammer.prover_result
 
-  val minimize_theorems :
-    params -> int -> int -> Proof.state -> (string * thm list) list
-    -> (string * thm list) list option * string
+  val run_minimizer : params -> int -> Facts.ref list -> Proof.state -> unit
 end;
 
 structure Sledgehammer_Fact_Minimizer : SLEDGEHAMMER_FACT_MINIMIZER =
@@ -20,6 +17,7 @@
 
 open Metis_Clauses
 open Sledgehammer_Util
+open Sledgehammer_Fact_Filter
 open Sledgehammer_Proof_Reconstruct
 open Sledgehammer
 
@@ -38,7 +36,6 @@
 fun sledgehammer_test_theorems (params : params) prover timeout subgoal state
                                filtered_clauses name_thms_pairs =
   let
-    val thy = Proof.theory_of state
     val num_theorems = length name_thms_pairs
     val _ =
       priority ("Testing " ^ string_of_int num_theorems ^
@@ -123,4 +120,17 @@
     handle ERROR msg => (NONE, "Error: " ^ msg)
   end
 
+fun run_minimizer params i refs state =
+  let
+    val ctxt = Proof.context_of state
+    val chained_ths = #facts (Proof.goal state)
+    val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs
+  in
+    case subgoal_count state of
+      0 => priority "No subgoal!"
+    | n =>
+      (kill_atps ();
+       priority (#2 (minimize_theorems params i n state name_thms_pairs)))
+  end
+
 end;
diff -r 463177795c49 -r f367847f5068 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 28 18:54:18 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 28 19:01:07 2010 +0200
@@ -19,7 +19,6 @@
 
 open ATP_Systems
 open Sledgehammer_Util
-open Sledgehammer_Fact_Filter
 open Sledgehammer
 open Sledgehammer_Fact_Minimizer
 
@@ -190,21 +189,6 @@
 
 (* Sledgehammer the given subgoal *)
 
-fun minimize override_params i refs state =
-  let
-    val thy = Proof.theory_of state
-    val ctxt = Proof.context_of state
-    val chained_ths = #facts (Proof.goal state)
-    val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs
-  in
-    case subgoal_count state of
-      0 => priority "No subgoal!"
-    | n =>
-      (kill_atps ();
-       priority (#2 (minimize_theorems (get_params thy override_params) i n
-                                       state name_thms_pairs)))
-  end
-
 val sledgehammerN = "sledgehammer"
 val sledgehammer_paramsN = "sledgehammer_params"
 
@@ -242,8 +226,9 @@
                          (minimize_command override_params i) state
       end
     else if subcommand = minimizeN then
-      minimize (map (apfst minimizize_raw_param_name) override_params)
-               (the_default 1 opt_i) (#add relevance_override) state
+      run_minimizer (get_params thy (map (apfst minimizize_raw_param_name)
+                                override_params))
+                    (the_default 1 opt_i) (#add relevance_override) state
     else if subcommand = messagesN then
       messages opt_i
     else if subcommand = available_atpsN then