diff -r e1ee4a9902bd -r 24bd1316eaae src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Mon Oct 12 07:25:38 2020 +0000
+++ b/src/HOL/Eisbach/method_closure.ML	Mon Oct 12 07:25:38 2020 +0000
@@ -178,7 +178,7 @@
   let
     val (uses_internal, lthy1) = lthy
       |> Proof_Context.concealed
-      |> Local_Theory.begin_target
+      |> Local_Theory.begin_nested
       |-> Proof_Context.private_scope
       |> Local_Theory.map_background_naming (Name_Space.add_path (Binding.name_of name))
       |> Config.put Method.old_section_parser true
@@ -221,7 +221,7 @@
     val term_args' = map (Morphism.term morphism) term_args;
   in
     lthy3
-    |> Local_Theory.close_target
+    |> Local_Theory.end_nested
     |> Proof_Context.restore_naming lthy
     |> put_closure name
         {vars = term_args', named_thms = named_thms, methods = method_args, body = text'}