diff -r 564ea783ace8 -r a010aab5bed0 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Wed Jan 21 23:40:23 2009 +0100
+++ b/src/HOL/Datatype.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -8,7 +8,7 @@
 header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
 
 theory Datatype
-imports Nat Relation
+imports Nat Product_Type
 begin
 
 typedef (Node)
@@ -509,15 +509,6 @@
 lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma, standard]
 
 
-(*** Domain ***)
-
-lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
-by auto
-
-lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
-by auto
-
-
 text {* hides popular names *}
 hide (open) type node item
 hide (open) const Push Node Atom Leaf Numb Lim Split Case