--- a/src/Pure/Isar/find_theorems.ML Fri Oct 21 18:14:51 2005 +0200
+++ b/src/Pure/Isar/find_theorems.ML Fri Oct 21 18:14:52 2005 +0200
@@ -9,7 +9,6 @@
signature FIND_THEOREMS =
sig
- val find_thms: Proof.context -> FactIndex.spec -> (thmref * thm) list
datatype 'term criterion =
Name of string | Intro | Elim | Dest | Simp of 'term | Pattern of 'term
val print_theorems: Proof.context -> term option -> int option ->
@@ -19,16 +18,6 @@
structure FindTheorems: FIND_THEOREMS =
struct
-
-(* find_thms *)
-
-fun find_thms ctxt spec =
- (PureThy.thms_containing (ProofContext.theory_of ctxt) spec @
- ProofContext.lthms_containing ctxt spec)
- |> map PureThy.selections |> List.concat;
-
-
-
(** search criteria **)
datatype 'term criterion =
@@ -245,6 +234,11 @@
(* print_theorems *)
+fun find_thms ctxt spec =
+ (PureThy.thms_containing (ProofContext.theory_of ctxt) spec @
+ ProofContext.lthms_containing ctxt spec)
+ |> map PureThy.selections |> List.concat;
+
fun print_theorems ctxt opt_goal opt_limit raw_criteria =
let
val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;