src/HOL/Datatype.thy

--- a/src/HOL/Datatype.thy	Thu Apr 24 16:53:04 2008 +0200
+++ b/src/HOL/Datatype.thy	Fri Apr 25 15:30:33 2008 +0200
@@ -9,7 +9,7 @@
 header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
 
 theory Datatype
-imports Finite_Set
+imports Finite_Set Wellfounded
 begin
 
 lemma size_bool [code func]: