Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
no explicit check for theory Nat
authorhaftmann
Wed, 22 Nov 2006 10:20:19 +0100
changeset 21459 20c2ddee8bc5
parent 21458 475b321982f7
child 21460 cda5cd8bfd16
no explicit check for theory Nat
src/HOL/Tools/datatype_package.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle