src/HOL/Tools/BNF/bnf_lfp_compat.ML

     |> Local_Theory.raw_theory register_interpret
     |> Local_Theory.notes all_notes
     |> snd
   end;
 
-val datatype_compat_global = map_local_theory o datatype_compat;
+val datatype_compat_global = Named_Target.theory_map o datatype_compat;
 
 fun datatype_compat_cmd raw_fpT_names lthy =
   let
     val fpT_names =
       map (fst o dest_Type o Proof_Context.read_type_name {proper = true, strict = false} lthy)

 
     val new_specs = map new_spec_of old_specs;
   in
     (fpT_names,
      thy
-     |> map_local_theory (co_datatypes Least_FP construct_lfp (default_ctr_options, new_specs))
+     |> Named_Target.theory_map
+       (co_datatypes Least_FP construct_lfp (default_ctr_options, new_specs))
      |> not (member (op =) prefs Keep_Nesting) ? perhaps (try (datatype_compat_global fpT_names)))
   end;
 
 val add_primrec = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec;
 val add_primrec_global = apfst (apsnd flat) ooo BNF_LFP_Rec_Sugar.add_primrec_global;