src/HOL/Inductive.thy
changeset 24845 abcd15369ffa
parent 24720 4d2f2e375fa1
child 24915 fc90277c0dd7
     1.1 --- a/src/HOL/Inductive.thy	Thu Oct 04 19:54:44 2007 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Thu Oct 04 19:54:46 2007 +0200
     1.3 @@ -17,7 +17,6 @@
     1.4    ("Tools/datatype_abs_proofs.ML")
     1.5    ("Tools/datatype_case.ML")
     1.6    ("Tools/datatype_package.ML")
     1.7 -  ("Tools/datatype_codegen.ML")
     1.8    ("Tools/primrec_package.ML")
     1.9  begin
    1.10  
    1.11 @@ -108,8 +107,6 @@
    1.12  use "Tools/datatype_package.ML"
    1.13  setup DatatypePackage.setup
    1.14  use "Tools/primrec_package.ML"
    1.15 -use "Tools/datatype_codegen.ML"
    1.16 -setup DatatypeCodegen.setup
    1.17  
    1.18  use "Tools/inductive_codegen.ML"
    1.19  setup InductiveCodegen.setup