src/HOL/Inductive.thy
changeset 37390 8781d80026fc
parent 35115 446c5063e4fd
child 39776 cde508d2eac8
     1.1 --- a/src/HOL/Inductive.thy	Thu Jun 10 12:24:01 2010 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Thu Jun 10 12:24:02 2010 +0200
     1.3 @@ -9,7 +9,6 @@
     1.4  uses
     1.5    ("Tools/inductive.ML")
     1.6    "Tools/dseq.ML"
     1.7 -  ("Tools/inductive_codegen.ML")
     1.8    "Tools/Datatype/datatype_aux.ML"
     1.9    "Tools/Datatype/datatype_prop.ML"
    1.10    "Tools/Datatype/datatype_case.ML"
    1.11 @@ -286,9 +285,6 @@
    1.12  use "Tools/old_primrec.ML"
    1.13  use "Tools/primrec.ML"
    1.14  
    1.15 -use "Tools/inductive_codegen.ML"
    1.16 -setup InductiveCodegen.setup
    1.17 -
    1.18  text{* Lambda-abstractions with pattern matching: *}
    1.19  
    1.20  syntax