src/HOL/Library/code_lazy.ML

     val freeT = HOLogic.unitT --> lazyT
     val lazyT' = Type (\<^type_name>\<open>lazy\<close>, [lazyT])
     val def = Logic.all_const freeT $ absdummy freeT (Logic.mk_equals (
       Free (name, (freeT --> eagerT)) $ Bound 0,
       lazy_ctr $ (Const (\<^const_name>\<open>delay\<close>, (freeT --> lazyT')) $ Bound 0)))
-    val lthy' = Local_Theory.open_target lthy
+    val lthy' = (snd o Local_Theory.begin_nested) lthy
     val ((t, (_, thm)), lthy') = Specification.definition NONE [] [] 
       ((Thm.def_binding (Binding.name name), []), def) lthy'
     val lthy' = Specification.notation true ("", false) [(t, Mixfix.mixfix "_")] lthy'
-    val lthy = Local_Theory.close_target lthy'
+    val lthy = Local_Theory.end_nested lthy'
     val def_thm = singleton (Proof_Context.export lthy' lthy) thm
   in
     (def_thm, lthy)
   end;
 

             { overloaded=false }
             (binding, rev (Term.add_tfreesT eager_type []), Mixfix.NoSyn)
             (Const (\<^const_name>\<open>top\<close>, Type (\<^type_name>\<open>set\<close>, [eager_type])))
             NONE
             (fn ctxt => resolve_tac ctxt [@{thm UNIV_witness}] 1)
-          o Local_Theory.open_target) lthy
-      in
-         (binding, result, Local_Theory.close_target lthy1)
+          o (snd o Local_Theory.begin_nested)) lthy
+      in
+         (binding, result, Local_Theory.end_nested lthy1)
       end;
 
     val (typedef_binding, (_, info), lthy2) = mk_lazy_typedef (short_lazy_type_name, eagerT) lthy1
 
     val lazy_type = Type (Local_Theory.full_name lthy2 typedef_binding, type_args)

 
     fun mk_def (name, T, rhs) lthy =
       let
         val binding = Binding.name name
         val ((_, (_, thm)), lthy1) = 
-          Local_Theory.open_target lthy
+          (snd o Local_Theory.begin_nested) lthy
           |> Specification.definition NONE [] [] ((Thm.def_binding binding, []), rhs)
-        val lthy2 = Local_Theory.close_target lthy1
+        val lthy2 = Local_Theory.end_nested lthy1
         val def_thm = hd (Proof_Context.export lthy1 lthy2 [thm])
       in
         ({binding = binding, const = Const (Local_Theory.full_name lthy2 binding, T), thm = def_thm}, lthy2)
       end;
     

         fun tac {context, ...} = Simplifier.simp_tac
           (put_simpset HOL_basic_ss context addsimps thms)
           1
         val thm = Goal.prove lthy [] [] term tac
         val (_, lthy1) = lthy
-          |> Local_Theory.open_target
+          |> (snd o Local_Theory.begin_nested)
           |> Local_Theory.note ((binding, []), [thm])
       in
-        (thm, Local_Theory.close_target lthy1)
+        (thm, Local_Theory.end_nested lthy1)
       end
     fun mk_thms exec_list lthy = fold_map mk_thm exec_list lthy
 
     val mk_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq