thms_containing: undeclared consts error;

--- 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]));