src/HOL/Typedef.thy
changeset 48891 c0eafbd55de3
parent 46950 d0181abdbdac
child 58239 1c5bc387bd4c
     1.1 --- a/src/HOL/Typedef.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Typedef.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -7,7 +7,6 @@
     1.4  theory Typedef
     1.5  imports Set
     1.6  keywords "typedef" :: thy_goal and "morphisms"
     1.7 -uses ("Tools/typedef.ML")
     1.8  begin
     1.9  
    1.10  locale type_definition =
    1.11 @@ -109,6 +108,6 @@
    1.12  
    1.13  end
    1.14  
    1.15 -use "Tools/typedef.ML" setup Typedef.setup
    1.16 +ML_file "Tools/typedef.ML" setup Typedef.setup
    1.17  
    1.18  end