src/Pure/theory.ML

 val subthy = Sign.subsig o pairself sign_of;
 val eq_thy = Sign.eq_sg o pairself sign_of;
 
 (*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 =
   if subthy (thy1, thy2) then thy2
   else raise THEORY ("Not a super theory", [thy1, thy2]);