| changeset 2863 | d97f5f424b97 |
| parent 1460 | 5a6f2aabd538 |
| child 3536 | 8fb4150e2ad3 |
--- 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);