# HG changeset patch
# User wenzelm
# Date 886156446 -3600
# Node ID 9f8f931e0089a04c7dcd52c087a2067275d279b0
# Parent  543e867efe40399fe893cba7f60c824aaeeae093
tuned msgs;

diff -r 543e867efe40 -r 9f8f931e0089 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Jan 30 11:33:01 1998 +0100
+++ b/src/Pure/pure_thy.ML	Fri Jan 30 11:34:06 1998 +0100
@@ -106,13 +106,13 @@
 
 fun get_thms thy name =
   (case all_local_thms (thy :: Theory.ancestors_of thy) name of
-    None => raise THEORY ("Theorems " ^ quote name ^ " not stored in theory", [thy])
+    None => raise THEORY ("Unknown theorem(s) " ^ quote name, [thy])
   | Some thms => thms);
 
 fun get_thm thy name =
   (case get_thms thy name of
     [thm] => thm
-  | _ => raise THEORY ("Singleton list of theorems expected " ^ quote name, [thy]));
+  | _ => raise THEORY ("Single theorem expected " ^ quote name, [thy]));
 
 
 (* thms_of *)