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
```