--- a/src/HOL/Eisbach/method_closure.ML Sat Oct 10 18:43:10 2020 +0000
+++ b/src/HOL/Eisbach/method_closure.ML Sat Oct 10 18:51:40 2020 +0000
@@ -178,7 +178,8 @@
let
val (uses_internal, lthy1) = lthy
|> Proof_Context.concealed
- |> Local_Theory.begin_target I |-> 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