| changeset 49636 | b7256a88a84b |
| parent 49591 | 91b228e26348 |
| child 49642 | 9f884142334c |
--- a/src/HOL/BNF/BNF_FP.thy Fri Sep 28 09:12:50 2012 +0200 +++ b/src/HOL/BNF/BNF_FP.thy Fri Sep 28 09:12:50 2012 +0200 @@ -121,7 +121,7 @@ unfolding sum_set_defs by simp+ ML_file "Tools/bnf_fp.ML" -ML_file "Tools/bnf_fp_sugar_tactics.ML" -ML_file "Tools/bnf_fp_sugar.ML" +ML_file "Tools/bnf_fp_def_sugar_tactics.ML" +ML_file "Tools/bnf_fp_def_sugar.ML" end