src/HOL/Inductive.thy

--- a/src/HOL/Inductive.thy	Tue Jul 10 17:30:47 2007 +0200
+++ b/src/HOL/Inductive.thy	Tue Jul 10 17:30:49 2007 +0200
@@ -6,7 +6,7 @@
 header {* Support for inductive sets and types *}
 
 theory Inductive 
-imports FixedPoint Sum_Type Relation Record
+imports FixedPoint Product_Type Sum_Type
 uses
   ("Tools/inductive_package.ML")
   ("Tools/old_inductive_package.ML")