no explicit check for theory Nat
authorhaftmann
Wed Nov 22 10:20:19 2006 +0100 (2006-11-22)
changeset 2145920c2ddee8bc5
parent 21458 475b321982f7
child 21460 cda5cd8bfd16
no explicit check for theory Nat
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Nov 22 10:20:18 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Nov 22 10:20:19 2006 +0100
     1.3 @@ -883,10 +883,8 @@
     1.4      val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
     1.5        [descr] sorts thy7;
     1.6      val (size_thms, thy9) =
     1.7 -      if Context.exists_name "Nat" thy8 then
     1.8 -        DatatypeAbsProofs.prove_size_thms false new_type_names
     1.9 -          [descr] sorts reccomb_names rec_thms thy8
    1.10 -      else ([], thy8);
    1.11 +      DatatypeAbsProofs.prove_size_thms false new_type_names
    1.12 +        [descr] sorts reccomb_names rec_thms thy8;
    1.13  
    1.14      val ((_, [induction']), thy10) =
    1.15        thy9