--- a/src/HOL/Product_Type.thy Mon Nov 13 15:43:07 2006 +0100
+++ b/src/HOL/Product_Type.thy Mon Nov 13 15:43:08 2006 +0100
@@ -7,7 +7,7 @@
header {* Cartesian products *}
theory Product_Type
-imports Fun
+imports Typedef Fun Code_Generator
uses ("Tools/split_rule.ML")
begin