src/HOL/Library/Old_Datatype.thy
changeset 58390 b74d8470b98e
parent 58377 c6f93b8d2d8e
child 58881 b9556a055632
     1.1 --- a/src/HOL/Library/Old_Datatype.thy	Fri Sep 19 13:27:04 2014 +0200
     1.2 +++ b/src/HOL/Library/Old_Datatype.thy	Fri Sep 19 13:27:04 2014 +0200
     1.3 @@ -10,7 +10,6 @@
     1.4  keywords "old_datatype" :: thy_decl
     1.5  begin
     1.6  
     1.7 -ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML"
     1.8  ML_file "~~/src/HOL/Tools/datatype_realizer.ML"
     1.9  
    1.10