# HG changeset patch
# User wenzelm
# Date 1201468894 -3600
# Node ID 928594f508935a98b5aca4690dfcd33cd634a1ef
# Parent  31b38a39e58978ce0912c20d8b41056b3b7e50a4
renamed thms_containing_limit to FindTheorems.limit;

diff -r 31b38a39e589 -r 928594f50893 src/Pure/Isar/find_theorems.ML
--- a/src/Pure/Isar/find_theorems.ML	Sun Jan 27 20:04:32 2008 +0100
+++ b/src/Pure/Isar/find_theorems.ML	Sun Jan 27 22:21:34 2008 +0100
@@ -5,10 +5,9 @@
 Retrieve theorems from proof context.
 *)
 
-val thms_containing_limit = ref 40;
-
 signature FIND_THEOREMS =
 sig
+  val limit: int ref
   datatype 'term criterion =
     Name of string | Intro | Elim | Dest | Simp of 'term | Pattern of 'term
   val print_theorems: Proof.context -> term option -> int option -> bool ->
@@ -287,6 +286,8 @@
     |> distinct (fn ((r1, th1), (r2, th2)) =>
         r1 = r2 andalso Thm.eq_thm_prop (th1, th2)));
 
+val limit = ref 40;
+
 fun print_theorems ctxt opt_goal opt_limit rem_dups raw_criteria =
   let
     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
@@ -299,8 +300,8 @@
       else raw_matches;
 
     val len = length matches;
-    val limit = the_default (! thms_containing_limit) opt_limit;
-    val thms = Library.drop (len - limit, matches);
+    val lim = the_default (! limit) opt_limit;
+    val thms = Library.drop (len - lim, matches);
 
     fun prt_fact (thmref, thm) =
       ProofContext.pretty_fact ctxt (PureThy.string_of_thmref thmref, [thm]);
@@ -309,7 +310,7 @@
      (if null thms then [Pretty.str "nothing found"]
       else
         [Pretty.str ("found " ^ string_of_int len ^ " theorems" ^
-          (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":"),
+          (if len <= lim then "" else " (" ^ string_of_int lim ^ " displayed)") ^ ":"),
          Pretty.str ""] @
         map prt_fact thms)
     |> Pretty.chunks |> Pretty.writeln