Made the error message more explicit
authorpaulson
Wed, 02 Apr 1997 11:33:14 +0200
changeset 2863 d97f5f424b97
parent 2862 3f38cbd57d47
child 2864 103bd2dc33b0
Made the error message more explicit
src/Pure/section_utils.ML
--- a/src/Pure/section_utils.ML	Wed Apr 02 11:32:48 1997 +0200
+++ b/src/Pure/section_utils.ML	Wed Apr 02 11:33:14 1997 +0200
@@ -67,4 +67,4 @@
 (*Check for some named theory*)
 fun require_thy thy name sect =
   if exists (equal name o !) (stamps_of_thy thy) then ()
-  else error ("Need at least theory " ^ quote name ^ " for " ^ sect);
+  else error ("Need theory " ^ quote name ^ " as an ancestor for " ^ sect);