src/HOL/Tools/BNF/bnf_def.ML

               ((if internal then Local_Theory.define_internal else Local_Theory.define)
                 ((b, NoSyn), ((Thm.def_binding b, []), rhs)) lthy)
           end
       end;
 
-    fun maybe_restore lthy_old lthy =
-      lthy |> not (Context.eq_thy (apply2 Proof_Context.theory_of (lthy_old, lthy)))
-        ? Local_Theory.restore;
-
     val map_bind_def =
       (fn () => def_qualify (if Binding.is_empty map_b then mk_prefix_binding mapN else map_b),
          map_rhs);
     val set_binds_defs =
       let

 
     val ((((bnf_map_term, raw_map_def),
       (bnf_set_terms, raw_set_defs)),
       (bnf_bd_term, raw_bd_def)), (lthy, lthy_old)) =
         no_defs_lthy
+        |> Local_Theory.open_target |> snd
         |> maybe_define true map_bind_def
         ||>> apfst split_list o fold_map (maybe_define true) set_binds_defs
         ||>> maybe_define true bd_bind_def
-        ||> `(maybe_restore no_defs_lthy);
+        ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
 
     val bnf_map_def = Morphism.thm phi raw_map_def;
     val bnf_set_defs = map (Morphism.thm phi) raw_set_defs;

           else map (fn i => fn () => def_qualify (mk_prefix_binding (mk_witN i))) (1 upto nwits);
       in bs ~~ wit_rhss end;
 
     val (((bnf_rel_term, raw_rel_def), (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) =
       lthy
+      |> Local_Theory.open_target |> snd
       |> maybe_define (is_some rel_rhs_opt) rel_bind_def
       ||>> apfst split_list o fold_map (maybe_define (not (null wit_rhss))) wit_binds_defs
-      ||> `(maybe_restore lthy);
+      ||> `Local_Theory.close_target;
 
     val phi = Proof_Context.export_morphism lthy_old lthy;
     val bnf_rel_def = Morphism.thm phi raw_rel_def;
     val bnf_rel = Morphism.term phi bnf_rel_term;
     fun mk_bnf_rel Ds As' Bs' =