src/HOL/datatype.ML

--- a/src/HOL/datatype.ML	Wed Apr 02 19:12:26 1997 +0200
+++ b/src/HOL/datatype.ML	Thu Apr 03 09:46:42 1997 +0200
@@ -138,6 +138,9 @@
 in
   fun add_datatype (typevars, tname, cons_list') thy = 
     let
+      val dummy = if length cons_list' < dtK then ()
+                  else require_thy thy "Nat" "datatype";
+      
       fun typid(dtRek(_,id)) = id
         | typid(dtVar s) = implode (tl (explode s))
         | typid(dtTyp(_,id)) = id;