diff -r f32fa5f5bdd1 -r 4d51ddd6aa5c 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]: