src/HOL/Tools/datatype_package.ML
changeset 10930 7c7a7b0e1d0c
parent 10911 eb5721204b38
child 11345 cd605c85e421
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Jan 18 20:36:08 2001 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Jan 18 20:36:31 2001 +0100
     1.3 @@ -716,7 +716,7 @@
     1.4      val (thy8, weak_case_congs) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
     1.5        [descr] sorts thy7;
     1.6      val (thy9, size_thms) =
     1.7 -      if exists (equal "NatArith") (Sign.stamp_names_of (Theory.sign_of thy8)) then
     1.8 +      if Sign.exists_stamp "NatArith" (Theory.sign_of thy8) then
     1.9          DatatypeAbsProofs.prove_size_thms false new_type_names
    1.10            [descr] sorts reccomb_names rec_thms thy8
    1.11        else (thy8, []);