src/HOL/Tools/BNF/bnf_lift.ML

     fun suffix tm s = (dest_Const tm |> fst |> Long_Name.base_name) ^ s;
     fun define lthy b n tm =
       let
         val b = Binding.qualify true absT_name (Binding.qualified_name b);
         val ((tm, (_, def)), (lthy, lthy_old)) = lthy
-          |> Local_Theory.open_target
+          |> (snd o Local_Theory.begin_nested)
           |> Local_Theory.define_internal (((Binding.concealed b, NoSyn), (Binding.empty_atts, tm)))
-          ||> `Local_Theory.close_target;
+          ||> `Local_Theory.end_nested;
         val phi = Proof_Context.export_morphism lthy_old lthy;
         val tm = Term.subst_atomic_types
           (map (`(Morphism.typ phi)) (alphas @ betas @ gammas @ map TFree Ds0))
           (Morphism.term phi tm);
         val def = mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi def));