diff -r fa30cd74d7d6 -r eb2f9d709296 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Jun 10 15:04:32 2009 +0200
+++ b/src/HOL/Product_Type.thy	Wed Jun 10 15:04:33 2009 +0200
@@ -12,7 +12,7 @@
   ("Tools/split_rule.ML")
   ("Tools/inductive_set_package.ML")
   ("Tools/inductive_realizer.ML")
-  ("Tools/datatype_realizer.ML")
+  ("Tools/datatype_package/datatype_realizer.ML")
 begin
 
 subsection {* @{typ bool} is a datatype *}
@@ -1155,7 +1155,7 @@
 use "Tools/inductive_set_package.ML"
 setup InductiveSetPackage.setup
 
-use "Tools/datatype_realizer.ML"
+use "Tools/datatype_package/datatype_realizer.ML"
 setup DatatypeRealizer.setup
 
 end