diff -r 9800a7602629 -r c6674504103f src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Tue Sep 25 10:27:43 2007 +0200
+++ b/src/HOL/Inductive.thy	Tue Sep 25 12:16:08 2007 +0200
@@ -6,18 +6,17 @@
 header {* Support for inductive sets and types *}
 
 theory Inductive 
-imports FixedPoint Product_Type Sum_Type
+imports FixedPoint Sum_Type
 uses
   ("Tools/inductive_package.ML")
-  ("Tools/inductive_set_package.ML")
-  ("Tools/inductive_realizer.ML")
+  (*("Tools/inductive_set_package.ML")
+  ("Tools/inductive_realizer.ML")*)
   "Tools/dseq.ML"
   ("Tools/inductive_codegen.ML")
   ("Tools/datatype_aux.ML")
   ("Tools/datatype_prop.ML")
   ("Tools/datatype_rep_proofs.ML")
   ("Tools/datatype_abs_proofs.ML")
-  ("Tools/datatype_realizer.ML")
   ("Tools/datatype_case.ML")
   ("Tools/datatype_package.ML")
   ("Tools/datatype_codegen.ML")
@@ -108,25 +107,15 @@
 use "Tools/datatype_rep_proofs.ML"
 use "Tools/datatype_abs_proofs.ML"
 use "Tools/datatype_case.ML"
-use "Tools/datatype_realizer.ML"
-
 use "Tools/datatype_package.ML"
 setup DatatypePackage.setup
-
+use "Tools/primrec_package.ML"
 use "Tools/datatype_codegen.ML"
 setup DatatypeCodegen.setup
 
-use "Tools/inductive_realizer.ML"
-setup InductiveRealizer.setup
-
 use "Tools/inductive_codegen.ML"
 setup InductiveCodegen.setup
 
-use "Tools/primrec_package.ML"
-
-use "Tools/inductive_set_package.ML"
-setup InductiveSetPackage.setup
-
 text{* Lambda-abstractions with pattern matching: *}
 
 syntax