# HG changeset patch
# User nipkow
# Date 860053602 -7200
# Node ID a0fde30aa126272959db71792da562b666710261
# Parent  477bfcb022d8dfff349897c6102b7784765527e8
Removed (Unit) in Prod.
Added test for ancestor Nat in datatype.

diff -r 477bfcb022d8 -r a0fde30aa126 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Wed Apr 02 19:12:26 1997 +0200
+++ b/src/HOL/Prod.ML	Thu Apr 03 09:46:42 1997 +0200
@@ -302,8 +302,8 @@
 
 goalw Prod.thy [Unity_def]
     "u = ()";
-by (stac (rewrite_rule [Unit_def] Rep_Unit RS CollectD RS sym) 1);
-by (rtac (Rep_Unit_inverse RS sym) 1);
+by (stac (rewrite_rule [unit_def] Rep_unit RS CollectD RS sym) 1);
+by (rtac (Rep_unit_inverse RS sym) 1);
 qed "unit_eq";
  
 AddIs  [fst_imageI, snd_imageI, prod_fun_imageI];
diff -r 477bfcb022d8 -r a0fde30aa126 src/HOL/Prod.thy
--- a/src/HOL/Prod.thy	Wed Apr 02 19:12:26 1997 +0200
+++ b/src/HOL/Prod.thy	Thu Apr 03 09:46:42 1997 +0200
@@ -79,14 +79,13 @@
 
 (** unit **)
 
-typedef (Unit)
-  unit = "{p. p = True}"
+typedef  unit = "{p. p = True}"
 
 consts
   "()"          :: unit                           ("'(')")
 
 defs
-  Unity_def     "() == Abs_Unit True"
+  Unity_def     "() == Abs_unit True"
 
 end
 
diff -r 477bfcb022d8 -r a0fde30aa126 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;