--- a/src/HOL/Eisbach/method_closure.ML Fri Aug 14 14:25:08 2020 +0200
+++ b/src/HOL/Eisbach/method_closure.ML Fri Aug 14 14:40:24 2020 +0200
@@ -178,7 +178,7 @@
let
val (uses_internal, lthy1) = lthy
|> Proof_Context.concealed
- |> Local_Theory.open_target |-> Proof_Context.private_scope
+ |> Local_Theory.begin_target |-> Proof_Context.private_scope
|> Local_Theory.map_background_naming (Name_Space.add_path (Binding.name_of name))
|> Config.put Method.old_section_parser true
|> fold setup_local_method methods