src/Pure/Tools/find_theorems.ML
changeset 41841 c27b0b37041a
parent 41835 9712fae15200
child 41844 b933142e02d0
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Fri Feb 25 08:46:52 2011 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Fri Feb 25 12:16:18 2011 +0100
     1.3 @@ -13,9 +13,11 @@
     1.4    val limit: int Unsynchronized.ref
     1.5    val find_theorems: Proof.context -> thm option -> int option -> bool ->
     1.6      (bool * string criterion) list -> int option * (Facts.ref * thm) list
     1.7 +  val filter_facts: Proof.context -> (Facts.ref * thm) list -> thm option ->
     1.8 +    int option -> bool -> (bool * string criterion) list ->
     1.9 +    int option * (Facts.ref * thm) list
    1.10 +
    1.11    val pretty_thm: Proof.context -> Facts.ref * thm -> Pretty.T
    1.12 -  val print_theorems: Proof.context -> thm option -> int option -> bool ->
    1.13 -    (bool * string criterion) list -> unit
    1.14  end;
    1.15  
    1.16  structure Find_Theorems: FIND_THEOREMS =
    1.17 @@ -388,7 +390,7 @@
    1.18  
    1.19  val limit = Unsynchronized.ref 40;
    1.20  
    1.21 -fun find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
    1.22 +fun filter_facts ctxt facts opt_goal opt_limit rem_dups raw_criteria =
    1.23    let
    1.24      val assms =
    1.25        ProofContext.get_fact ctxt (Facts.named "local.assms")
    1.26 @@ -417,19 +419,19 @@
    1.27        then find_all
    1.28        else pair NONE o Seq.list_of o Seq.take (the opt_limit) o lazy_filter filters;
    1.29  
    1.30 -  in find (all_facts_of ctxt) end;
    1.31 +  in find facts end;
    1.32  
    1.33 +fun find_theorems ctxt = filter_facts ctxt (all_facts_of ctxt)
    1.34  
    1.35  fun pretty_thm ctxt (thmref, thm) = Pretty.block
    1.36    [Pretty.str (Facts.string_of_ref thmref), Pretty.str ":", Pretty.brk 1,
    1.37      Display.pretty_thm ctxt thm];
    1.38  
    1.39 -fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
    1.40 +fun print_theorems ctxt (foundo, thms) raw_criteria =
    1.41    let
    1.42      val start = start_timing ();
    1.43  
    1.44      val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
    1.45 -    val (foundo, thms) = find_theorems ctxt opt_goal opt_limit rem_dups raw_criteria;
    1.46      val returned = length thms;
    1.47  
    1.48      val tally_msg =
    1.49 @@ -484,7 +486,8 @@
    1.50            let
    1.51              val ctxt = Toplevel.context_of state;
    1.52              val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
    1.53 -          in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
    1.54 +            val found = find_theorems ctxt opt_goal opt_lim rem_dups spec;
    1.55 +          in print_theorems ctxt found spec end)));
    1.56  
    1.57  end;
    1.58