# HG changeset patch
# User paulson
# Date 859973594 -7200
# Node ID d97f5f424b979bc0a9b21d94c8f56b80163b3bdc
# Parent  3f38cbd57d470f697baf18363c9907d549d32435
Made the error message more explicit

diff -r 3f38cbd57d47 -r d97f5f424b97 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);