| changeset 58376 | c9d3074f83b3 |
| parent 58352 | 37745650a3f4 |
| child 58377 | c6f93b8d2d8e |
--- a/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 18 16:47:40 2014 +0200 +++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 18 16:47:40 2014 +0200 @@ -232,7 +232,6 @@ ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML" ML_file "Tools/BNF/bnf_lfp_size.ML" ML_file "Tools/Function/old_size.ML" -ML_file "Tools/datatype_realizer.ML" hide_fact (open) id_transfer