# HG changeset patch
# User noschinl
# Date 1298632578 -3600
# Node ID c27b0b37041aa8f00fc1e03d1722ccc52e9bb523
# Parent  f69045fdc836fd2119553b43d31d8d65fb7a3dd0
Refactor find_theorems to provide a more general filter_facts method

diff -r f69045fdc836 -r c27b0b37041a src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Fri Feb 25 08:46:52 2011 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Fri Feb 25 12:16:18 2011 +0100
@@ -13,9 +13,11 @@
   val limit: int Unsynchronized.ref
   val find_theorems: Proof.context -> thm option -> int option -> bool ->
     (bool * string criterion) list -> int option * (Facts.ref * thm) list
+  val filter_facts: Proof.context -> (Facts.ref * thm) list -> thm option ->
+    int option -> bool -> (bool * string criterion) list ->
+    int option * (Facts.ref * thm) list
+
   val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
-  val print_theorems: Proof.context -> thm option -> int option -> bool ->
-    (bool * string criterion) list -> unit
 end;
 
 structure Find_Theorems: FIND_THEOREMS =
@@ -388,7 +390,7 @@
 
 val limit = Unsynchronized.ref 40;
 
-fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
+fun filter_facts ctxt facts opt_goal opt_limit rem_dups raw_criteria =
   let
     val assms =
       ProofContext.get_fact ctxt (Facts.named "local.assms")
@@ -417,19 +419,19 @@
       then find_all
       else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters;
 
-  in find (all_facts_of ctxt) end;
+  in find facts end;
 
+fun find_theorems ctxt = filter_facts ctxt (all_facts_of ctxt)
 
 fun pretty_thm ctxt (thmref, thm) = Pretty.block
   [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
     Display.pretty_thm ctxt thm];
 
-fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
+fun print_theorems ctxt (foundo, thms) raw_criteria =
   let
     val start = start_timing ();
 
     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
-    val (foundo, thms) = find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria;
     val returned = length thms;
 
     val tally_msg =
@@ -484,7 +486,8 @@
           let
             val ctxt = Toplevel.context_of state;
             val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
-          in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
+            val found = find_theorems ctxt opt_goal opt_lim rem_dups spec;
+          in print_theorems ctxt found spec end)));
 
 end;