changeset 58376 | c9d3074f83b3 |
parent 58372 | bfd497f2f4c2 |
child 58377 | c6f93b8d2d8e |
--- a/src/HOL/Library/Old_Datatype.thy Thu Sep 18 16:47:40 2014 +0200 +++ b/src/HOL/Library/Old_Datatype.thy Thu Sep 18 16:47:40 2014 +0200 @@ -523,5 +523,6 @@ ML_file "~~/src/HOL/Tools/Old_Datatype/old_datatype.ML" ML_file "~~/src/HOL/Tools/inductive_realizer.ML" +ML_file "~~/src/HOL/Tools/datatype_realizer.ML" end