# HG changeset patch
# User wenzelm
# Date 939392211 -7200
# Node ID 0ae9ddc36fe0c38204d452045d07962dbdce756f
# Parent  80706fa8462297d4af7a6c15934e98579bdd025e
theorem database now also indexes constants "Trueprop", "all",
"==>", "=="; thus thms_containing, findI etc. may retrieve more rules;

diff -r 80706fa84622 -r 0ae9ddc36fe0 NEWS
--- a/NEWS	Fri Oct 08 16:05:06 1999 +0200
+++ b/NEWS	Fri Oct 08 16:16:51 1999 +0200
@@ -119,6 +119,9 @@
 result is not stored, but proper checks and presentation of the result
 still apply;
 
+* theorem database now also indexes constants "Trueprop", "all",
+"==>", "=="; thus thms_containing, findI etc. may retrieve more rules;
+
 
 *** HOL ***
 
diff -r 80706fa84622 -r 0ae9ddc36fe0 doc-src/Ref/goals.tex
--- a/doc-src/Ref/goals.tex	Fri Oct 08 16:05:06 1999 +0200
+++ b/doc-src/Ref/goals.tex	Fri Oct 08 16:16:51 1999 +0200
@@ -287,9 +287,8 @@
   premise of subgoal $i$.  Useful in connection with \texttt{eresolve_tac} and
   \texttt{dresolve_tac}.
   
-\item[\ttindexbold{thms_containing} $consts$] returns all theorems
-  that contain all of a given set of constants.  Note that a few basic
-  constants like \verb$==>$ are ignored.
+\item[\ttindexbold{thms_containing} $consts$] returns all theorems that
+  contain \emph{all} of the given constants.
 \end{ttdescription}
 
 
diff -r 80706fa84622 -r 0ae9ddc36fe0 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Oct 08 16:05:06 1999 +0200
+++ b/src/Pure/pure_thy.ML	Fri Oct 08 16:16:51 1999 +0200
@@ -141,13 +141,11 @@
 
 (* make index *)
 
-val ignore = ["Trueprop", "all", "==>", "=="];
-
 fun add_const_idx ((next, table), thm) =
   let
     val {hyps, prop, ...} = Thm.rep_thm thm;
     val consts =
-      foldr add_term_consts (hyps, add_term_consts (prop, [])) \\ ignore;
+      foldr add_term_consts (hyps, add_term_consts (prop, []));
 
     fun add (tab, c) =
       Symtab.update ((c, (next, thm) :: Symtab.lookup_multi (tab, c)), tab);
@@ -180,7 +178,7 @@
 (*search globally*)
 fun thms_containing thy consts =
   (case filter (is_none o Sign.const_type (Theory.sign_of thy)) consts of
-    [] => flat (map (containing (consts \\ ignore)) (thy :: Theory.ancestors_of thy))
+    [] => flat (map (containing consts) (thy :: Theory.ancestors_of thy))
   | cs => raise THEORY ("thms_containing: undeclared consts " ^ commas_quote cs, [thy]));