# HG changeset patch
# User clasohm
# Date 801752667 -7200
# Node ID 5e9775c196e8c408c3e6618337bdb025a055a7e7
# Parent  28e312a189461d3e7ee6b31a650739173bf9161c
changed error message in thms_containing

diff -r 28e312a18946 -r 5e9775c196e8 src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Mon May 29 14:12:48 1995 +0200
+++ b/src/Pure/Thy/thm_database.ML	Mon May 29 15:04:27 1995 +0200
@@ -74,9 +74,10 @@
                                           else (result desc_inter new_thms))
             end;
 
-      val ignored = constants inter ignore;
-  in if null ignored then () else
-       error ("The following constant(s) must not be used for searching the \
-              \theorem database:\n  " ^ commas (map quote ignored));
-     collect constants true [] end;
+      val look_for = constants \\ ignore;
+  in if null look_for then
+       error ("Only ignored constants specified for theorem database search:\n"
+              ^ commas (map quote ignored))
+     else ();
+     collect look_for true [] end;
 end;