--- a/src/HOL/Product_Type.thy Sat Oct 24 17:49:44 2009 +0200
+++ b/src/HOL/Product_Type.thy Sat Oct 24 18:55:27 2009 +0200
@@ -6,7 +6,7 @@
header {* Cartesian products *}
theory Product_Type
-imports Inductive
+imports Inductive Nat
uses
("Tools/split_rule.ML")
("Tools/inductive_set.ML")