parameterize print_theorems over actual search function
authorkrauss
Mon May 30 17:07:48 2011 +0200 (2011-05-30)
changeset 430767b06cd71792c
parent 43075 6fde0c323c15
child 43078 e2631aaf1e1e
parameterize print_theorems over actual search function
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon May 30 17:07:48 2011 +0200
     1.3 @@ -581,12 +581,12 @@
     1.4  
     1.5  fun pretty_thm ctxt (thmref, thm) = pretty_theorem ctxt (Internal (thmref, thm));
     1.6  
     1.7 -fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
     1.8 +fun gen_print_theorems find ctxt opt_goal opt_limit rem_dups raw_criteria =
     1.9    let
    1.10      val start = Timing.start ();
    1.11  
    1.12      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
    1.13 -    val (foundo, theorems) = filter_theorems ctxt (map Internal (all_facts_of ctxt))
    1.14 +    val (foundo, theorems) = find
    1.15        {goal=opt_goal, limit=opt_limit, rem_dups=rem_dups, criteria=criteria};
    1.16      val returned = length theorems;
    1.17  
    1.18 @@ -609,6 +609,8 @@
    1.19          map (pretty_theorem ctxt) theorems)
    1.20    end |> Pretty.chunks |> Pretty.writeln;
    1.21  
    1.22 +fun print_theorems ctxt =
    1.23 +  gen_print_theorems (filter_theorems ctxt (map Internal (all_facts_of ctxt))) ctxt;
    1.24  
    1.25  
    1.26  (** command syntax **)