src/HOL/Typedef.thy
changeset 38536 7e57a0dcbd4f
parent 38393 7c045c03598f
child 41732 996b0c14a430
     1.1 --- a/src/HOL/Typedef.thy	Tue Aug 17 16:44:21 2010 +0200
     1.2 +++ b/src/HOL/Typedef.thy	Tue Aug 17 16:44:24 2010 +0200
     1.3 @@ -6,9 +6,7 @@
     1.4  
     1.5  theory Typedef
     1.6  imports Set
     1.7 -uses
     1.8 -  ("Tools/typedef.ML")
     1.9 -  ("Tools/typedef_codegen.ML")
    1.10 +uses ("Tools/typedef.ML")
    1.11  begin
    1.12  
    1.13  ML {*
    1.14 @@ -115,6 +113,5 @@
    1.15  end
    1.16  
    1.17  use "Tools/typedef.ML" setup Typedef.setup
    1.18 -use "Tools/typedef_codegen.ML" setup TypedefCodegen.setup
    1.19  
    1.20  end