src/HOL/Tools/datatype_package.ML

--- a/src/HOL/Tools/datatype_package.ML	Wed Nov 08 11:23:09 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Wed Nov 08 13:48:29 2006 +0100
@@ -877,7 +877,7 @@
     val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
       [descr] sorts thy7;
     val (size_thms, thy9) =
-      if Context.exists_name "NatArith" thy8 then
+      if Context.exists_name "Nat" thy8 then
         DatatypeAbsProofs.prove_size_thms false new_type_names
           [descr] sorts reccomb_names rec_thms thy8
       else ([], thy8);