# HG changeset patch
# User krauss
# Date 1306768068 -7200
# Node ID 7b06cd71792cf495ea32f22c6d7db6334026432f
# Parent  6fde0c323c1558ac1ba229f0b8a4d2166e37fb93
parameterize print_theorems over actual search function

diff -r 6fde0c323c15 -r 7b06cd71792c src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
@@ -581,12 +581,12 @@
 
 fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
 
-fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
+fun gen_print_theorems find ctxt opt_goal opt_limit rem_dups raw_criteria =
   let
     val start = Timing.start ();
 
     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
-    val (foundo, theorems) = filter_theorems ctxt (map Internal (all_facts_of ctxt))
+    val (foundo, theorems) = find
       {goal=opt_goal, limit=opt_limit, rem_dups=rem_dups, criteria=criteria};
     val returned = length theorems;
 
@@ -609,6 +609,8 @@
         map (pretty_theorem ctxt) theorems)
   end |> Pretty.chunks |> Pretty.writeln;
 
+fun print_theorems ctxt =
+  gen_print_theorems (filter_theorems ctxt (map Internal (all_facts_of ctxt))) ctxt;
 
 
 (** command syntax **)