# HG changeset patch
# User berghofe
# Date 1007993869 -3600
# Node ID 6d4e02b6dd43ca57bed2eb5f1eb149c94e17f2fc
# Parent  a2df07fefed7b692a323dbef42e39f29610b96dc
Moved code generator setup from Recdef to Inductive.

diff -r a2df07fefed7 -r 6d4e02b6dd43 src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Mon Dec 10 15:16:49 2001 +0100
+++ b/src/HOL/Inductive.thy	Mon Dec 10 15:17:49 2001 +0100
@@ -9,11 +9,14 @@
 theory Inductive = Gfp + Sum_Type + Relation
 files
   ("Tools/inductive_package.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_package.ML")
+  ("Tools/datatype_codegen.ML")
+  ("Tools/recfun_codegen.ML")
   ("Tools/primrec_package.ML"):
 
 
@@ -69,6 +72,9 @@
 
 text {* Package setup. *}
 
+use "Tools/recfun_codegen.ML"
+setup RecfunCodegen.setup
+
 use "Tools/datatype_aux.ML"
 use "Tools/datatype_prop.ML"
 use "Tools/datatype_rep_proofs.ML"
@@ -76,7 +82,12 @@
 use "Tools/datatype_package.ML"
 setup DatatypePackage.setup
 
+use "Tools/datatype_codegen.ML"
+setup DatatypeCodegen.setup
+
+use "Tools/inductive_codegen.ML"
+setup InductiveCodegen.setup
+
 use "Tools/primrec_package.ML"
-setup PrimrecPackage.setup
 
 end
diff -r a2df07fefed7 -r 6d4e02b6dd43 src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Mon Dec 10 15:16:49 2001 +0100
+++ b/src/HOL/Recdef.thy	Mon Dec 10 15:17:49 2001 +0100
@@ -15,9 +15,7 @@
   ("../TFL/thry.ML")
   ("../TFL/tfl.ML")
   ("../TFL/post.ML")
-  ("Tools/recdef_package.ML")
-  ("Tools/basic_codegen.ML")
-  ("Tools/inductive_codegen.ML"):
+  ("Tools/recdef_package.ML"):
 
 lemma tfl_eq_True: "(x = True) --> x"
   by blast
@@ -52,11 +50,7 @@
 use "../TFL/tfl.ML"
 use "../TFL/post.ML"
 use "Tools/recdef_package.ML"
-use "Tools/basic_codegen.ML"
-use "Tools/inductive_codegen.ML"
 setup RecdefPackage.setup
-setup BasicCodegen.setup
-setup InductiveCodegen.setup
 
 lemmas [recdef_simp] =
   inv_image_def