# HG changeset patch
# User wenzelm
# Date 979846591 -3600
# Node ID 7c7a7b0e1d0cd61d59428f445f664d60702acefe
# Parent  ccceb5fb517dbff68a6f947e83d3057324c97ae6
Sign.exists_stamp;

diff -r ccceb5fb517d -r 7c7a7b0e1d0c src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Thu Jan 18 20:36:08 2001 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Thu Jan 18 20:36:31 2001 +0100
@@ -716,7 +716,7 @@
     val (thy8, weak_case_congs) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
       [descr] sorts thy7;
     val (thy9, size_thms) =
-      if exists (equal "NatArith") (Sign.stamp_names_of (Theory.sign_of thy8)) then
+      if Sign.exists_stamp "NatArith" (Theory.sign_of thy8) then
         DatatypeAbsProofs.prove_size_thms false new_type_names
           [descr] sorts reccomb_names rec_thms thy8
       else (thy8, []);
diff -r ccceb5fb517d -r 7c7a7b0e1d0c src/Pure/theory.ML
--- 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 =