# 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