src/HOL/Tools/BNF/bnf_lfp_size.ML

 
       val nested_size_gen_o_maps_complete = forall (not o null) nested_size_gen_o_mapss;
       val nested_size_gen_o_maps = fold (union Thm.eq_thm_prop) nested_size_gen_o_mapss [];
 
       val ((raw_size_consts, raw_size_defs), (lthy1, lthy1_old)) = lthy0
-        |> Local_Theory.open_target
+        |> (snd o Local_Theory.begin_nested)
         |> apfst split_list o @{fold_map 2} (fn b => fn rhs =>
             Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs))
             #>> apsnd snd)
           size_bs size_rhss
-        ||> `Local_Theory.close_target;
+        ||> `Local_Theory.end_nested;
 
       val phi = Proof_Context.export_morphism lthy1_old lthy1;
 
       val size_defs = map (Morphism.thm phi) raw_size_defs;