--- a/src/HOL/Product_Type.thy Tue Jun 05 12:12:25 2007 +0200
+++ b/src/HOL/Product_Type.thy Tue Jun 05 15:16:08 2007 +0200
@@ -7,7 +7,7 @@
header {* Cartesian products *}
theory Product_Type
-imports Typedef Fun Code_Generator
+imports Typedef Fun
uses ("Tools/split_rule.ML")
begin