# HG changeset patch
# User wenzelm
# Date 931811011 -7200
# Node ID 4781c0673e83da38a32a1a1de7563af0b286d179
# Parent  3895ba31db711899d962a2af690b525ab26bb528
thms_containing: undeclared consts error;

diff -r 3895ba31db71 -r 4781c0673e83 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Mon Jul 12 22:23:07 1999 +0200
+++ b/src/Pure/pure_thy.ML	Mon Jul 12 22:23:31 1999 +0200
@@ -189,13 +189,13 @@
 
         val ref {const_idx = (_, ctab), ...} = get_theorems thy;
         val ithmss = map (fn c => Symtab.lookup_multi (ctab, c)) consts;
-      in
-        map (attach_name o snd) (ints ithmss)
-      end;
+      in map (attach_name o snd) (ints ithmss) end;
 
 (*search globally*)
 fun thms_containing thy consts =
-  flat (map (containing (consts \\ ignore)) (thy :: Theory.ancestors_of thy));
+  (case filter (is_none o Sign.const_type (Theory.sign_of thy)) consts of
+    [] => flat (map (containing (consts \\ ignore)) (thy :: Theory.ancestors_of thy))
+  | cs => raise THEORY ("thms_containing: undeclared consts " ^ commas_quote cs, [thy]));