src/HOL/Tools/BNF/bnf_lfp_compat.ML

     |> Local_Theory.raw_theory register_interpret
     |> Local_Theory.notes all_notes
     |> snd
   end;
 
-fun datatype_compat_global fpT_names =
-  Named_Target.theory_init
-  #> datatype_compat fpT_names
-  #> Named_Target.exit;
+val datatype_compat_global = map_local_theory 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
-     |> Named_Target.theory_init
-     |> co_datatypes Least_FP construct_lfp ((false, false), new_specs)
-     |> Named_Target.exit
+     |> map_local_theory (co_datatypes Least_FP construct_lfp ((false, false), new_specs))
      |> nesting_pref = Unfold_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;