diff -r a6c3962ea907 -r d2ddd401d74d src/HOL/Inductive.thy
--- a/src/HOL/Inductive.thy	Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Inductive.thy	Fri Sep 05 00:41:01 2014 +0200
@@ -273,7 +273,7 @@
 
 ML_file "Tools/Old_Datatype/old_datatype_aux.ML"
 ML_file "Tools/Old_Datatype/old_datatype_prop.ML"
-ML_file "Tools/Old_Datatype/old_datatype_data.ML" setup Old_Datatype_Data.setup
+ML_file "Tools/Old_Datatype/old_datatype_data.ML"
 ML_file "Tools/Old_Datatype/old_rep_datatype.ML"
 ML_file "Tools/Old_Datatype/old_datatype_codegen.ML"
 ML_file "Tools/Old_Datatype/old_primrec.ML"