# 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;