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