src/HOL/Tools/datatype_package.ML

     val (thy7, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names
       [descr] sorts nchotomys case_thms thy6;
     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, []);
 
     val (thy10, [induction']) = thy9 |>