src/HOL/Datatype.thy
changeset 48891 c0eafbd55de3
parent 47488 be6dd389639d
child 49834 b27bbb021df1
     1.1 --- a/src/HOL/Datatype.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -8,10 +8,6 @@
     1.4  theory Datatype
     1.5  imports Product_Type Sum_Type Nat
     1.6  keywords "datatype" :: thy_decl
     1.7 -uses
     1.8 -  ("Tools/Datatype/datatype.ML")
     1.9 -  ("Tools/inductive_realizer.ML")
    1.10 -  ("Tools/Datatype/datatype_realizer.ML")
    1.11  begin
    1.12  
    1.13  subsection {* The datatype universe *}
    1.14 @@ -517,12 +513,12 @@
    1.15  hide_type (open) node item
    1.16  hide_const (open) Push Node Atom Leaf Numb Lim Split Case
    1.17  
    1.18 -use "Tools/Datatype/datatype.ML"
    1.19 +ML_file "Tools/Datatype/datatype.ML"
    1.20  
    1.21 -use "Tools/inductive_realizer.ML"
    1.22 +ML_file "Tools/inductive_realizer.ML"
    1.23  setup InductiveRealizer.setup
    1.24  
    1.25 -use "Tools/Datatype/datatype_realizer.ML"
    1.26 +ML_file "Tools/Datatype/datatype_realizer.ML"
    1.27  setup Datatype_Realizer.setup
    1.28  
    1.29  end