src/Pure/theory.ML
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 =