changeset 55571 | a6153343c44f |
parent 55538 | 6a5986170c1d |
child 55575 | a5e33e18fb5c |
--- a/src/HOL/BNF_LFP.thy Tue Feb 18 23:08:58 2014 +0100 +++ b/src/HOL/BNF_LFP.thy Tue Feb 18 23:08:59 2014 +0100 @@ -241,8 +241,8 @@ ML_file "Tools/BNF/bnf_lfp_tactics.ML" ML_file "Tools/BNF/bnf_lfp.ML" ML_file "Tools/BNF/bnf_lfp_compat.ML" -ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML" ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML" +ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML" hide_fact (open) id_transfer