src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML
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));