--- a/src/HOL/Inductive.thy Wed Nov 13 15:24:42 2002 +0100
+++ b/src/HOL/Inductive.thy Wed Nov 13 15:25:17 2002 +0100
@@ -9,6 +9,7 @@
theory Inductive = Gfp + Sum_Type + Relation + Record
files
("Tools/inductive_package.ML")
+ ("Tools/inductive_realizer.ML")
("Tools/inductive_codegen.ML")
("Tools/datatype_aux.ML")
("Tools/datatype_prop.ML")
@@ -87,6 +88,9 @@
use "Tools/datatype_codegen.ML"
setup DatatypeCodegen.setup
+use "Tools/inductive_realizer.ML"
+setup InductiveRealizer.setup
+
use "Tools/inductive_codegen.ML"
setup InductiveCodegen.setup