changeset 58665 | 50b229a5a097 |
parent 58585 | efc8b2c54a38 |
child 58671 | 4cc24f1e52d5 |
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 13 20:51:48 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 13 21:41:29 2014 +0200 @@ -176,7 +176,7 @@ set_inducts = []}} end; -val _ = Theory.setup (map_local_theory (fn lthy => +val _ = Theory.setup (Named_Target.theory_map (fn lthy => fold (BNF_FP_Def_Sugar.register_fp_sugars (K true) o single o (fn f => f lthy)) [fp_sugar_of_sum, fp_sugar_of_prod] lthy));