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