changeset 10930 | 7c7a7b0e1d0c |
parent 10494 | 305b37c8d8a3 |
child 11501 | 3b6415035d1a |
--- a/src/Pure/theory.ML Thu Jan 18 20:36:08 2001 +0100 +++ b/src/Pure/theory.ML Thu Jan 18 20:36:31 2001 +0100 @@ -141,7 +141,7 @@ (*check for some theory*) fun requires thy name what = - if exists (equal name) (Sign.stamp_names_of (sign_of thy)) then () + if Sign.exists_stamp name (sign_of thy) then () else error ("Require theory " ^ quote name ^ " as an ancestor for " ^ what); fun assert_super thy1 thy2 =