--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Jun 05 07:52:45 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sat Jun 05 15:07:50 2010 +0200
@@ -19,6 +19,7 @@
struct
open Sledgehammer_Util
+open Sledgehammer_Fact_Filter
open Sledgehammer_Fact_Preprocessor
open ATP_Manager
open ATP_Systems
@@ -238,19 +239,12 @@
state) atps
in () end
-fun minimize override_params i frefs state =
+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)
- fun theorems_from_ref ctxt fref =
- let
- val ths = ProofContext.get_fact ctxt fref
- val name = Facts.string_of_ref fref
- |> forall (member Thm.eq_thm chained_ths) ths
- ? prefix chained_prefix
- in (name, ths) end
- val name_thms_pairs = map (theorems_from_ref ctxt) frefs
+ val name_thms_pairs = map (name_thms_pair_from_ref ctxt chained_ths) refs
in
case subgoal_count state of
0 => priority "No subgoal!"