src/HOL/Inductive.thy
changeset 24626 85eceef2edc7
parent 24625 0398a5e802d3
child 24699 c6674504103f
     1.1 --- a/src/HOL/Inductive.thy	Tue Sep 18 07:36:38 2007 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Tue Sep 18 07:46:00 2007 +0200
     1.3 @@ -18,7 +18,6 @@
     1.4    ("Tools/datatype_rep_proofs.ML")
     1.5    ("Tools/datatype_abs_proofs.ML")
     1.6    ("Tools/datatype_realizer.ML")
     1.7 -  ("Tools/datatype_hooks.ML")
     1.8    ("Tools/datatype_case.ML")
     1.9    ("Tools/datatype_package.ML")
    1.10    ("Tools/datatype_codegen.ML")
    1.11 @@ -111,8 +110,6 @@
    1.12  use "Tools/datatype_case.ML"
    1.13  use "Tools/datatype_realizer.ML"
    1.14  
    1.15 -use "Tools/datatype_hooks.ML"
    1.16 -
    1.17  use "Tools/datatype_package.ML"
    1.18  setup DatatypePackage.setup
    1.19