diff -r 0a3adceb9c67 -r 36c0a6dd8c6f src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Feb 12 09:49:28 2010 +0100
+++ b/src/HOL/Nat.thy	Fri Feb 12 14:28:01 2010 +0100
@@ -8,7 +8,7 @@
 header {* Natural numbers *}
 
 theory Nat
-imports Inductive Product_Type Fields
+imports Inductive Typedef Fun Fields
 uses
   "~~/src/Tools/rat.ML"
   "~~/src/Provers/Arith/cancel_sums.ML"