diff -r 745799215e02 -r b5eb0b4dd17d 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")