# HG changeset patch
# User wenzelm
# Date 1129911292 -7200
# Node ID 4969d6eb4c97c499436814ecf00fc7b02d9186d2
# Parent  ffcec1ddbc1e76416c76433e44c62f94be1bf1fd
do not export find_thms;

diff -r ffcec1ddbc1e -r 4969d6eb4c97 src/Pure/Isar/find_theorems.ML
--- 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;