src/HOL/Datatype.thy
changeset 19770 be5c23ebe1eb
parent 19564 d3e2f532459a
child 19787 b949911ecff5
     1.1 --- a/src/HOL/Datatype.thy	Mon Jun 05 14:22:58 2006 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Mon Jun 05 14:26:07 2006 +0200
     1.3 @@ -6,8 +6,7 @@
     1.4  header {* Datatypes *}
     1.5  
     1.6  theory Datatype
     1.7 -imports Datatype_Universe FunDef
     1.8 -uses ("Tools/function_package/fundef_datatype.ML")
     1.9 +imports Datatype_Universe
    1.10  begin
    1.11  
    1.12  subsection {* Representing primitive types *}
    1.13 @@ -316,8 +315,6 @@
    1.14      haskell (target_atom "Just")
    1.15  
    1.16  
    1.17 -use "Tools/function_package/fundef_datatype.ML"
    1.18 -setup FundefDatatype.setup
    1.19  
    1.20  
    1.21  end