# HG changeset patch
# User haftmann
# Date 1164187219 -3600
# Node ID 20c2ddee8bc58fee5ef7fb08962a83470d60d02b
# Parent  475b321982f772d8a4b7b8883378dc3ee0e42cde
no explicit check for theory Nat

diff -r 475b321982f7 -r 20c2ddee8bc5 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Wed Nov 22 10:20:18 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Wed Nov 22 10:20:19 2006 +0100
@@ -883,10 +883,8 @@
     val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
       [descr] sorts thy7;
     val (size_thms, thy9) =
-      if Context.exists_name "Nat" thy8 then
-        DatatypeAbsProofs.prove_size_thms false new_type_names
-          [descr] sorts reccomb_names rec_thms thy8
-      else ([], thy8);
+      DatatypeAbsProofs.prove_size_thms false new_type_names
+        [descr] sorts reccomb_names rec_thms thy8;
 
     val ((_, [induction']), thy10) =
       thy9