# HG changeset patch
# User haftmann
# Date 1602355387 0
# Node ID 7e0e497dacbc2b3528182fc6d37fbb3197eb46a9
# Parent  86f8fcdcff4af329f03c6ed9f8fe5bb26d9b5b8e
avoid baroque export

diff -r 86f8fcdcff4a -r 7e0e497dacbc src/HOL/Eisbach/method_closure.ML
--- a/src/HOL/Eisbach/method_closure.ML	Sat Oct 10 22:06:17 2020 +0200
+++ b/src/HOL/Eisbach/method_closure.ML	Sat Oct 10 18:43:07 2020 +0000
@@ -178,7 +178,7 @@
   let
     val (uses_internal, lthy1) = lthy
       |> Proof_Context.concealed
-      |> Local_Theory.begin_target |-> Proof_Context.private_scope
+      |> Local_Theory.begin_target I |-> 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
diff -r 86f8fcdcff4a -r 7e0e497dacbc src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Sat Oct 10 22:06:17 2020 +0200
+++ b/src/Pure/Isar/bundle.ML	Sat Oct 10 18:43:07 2020 +0000
@@ -215,9 +215,7 @@
       |> gen_includes get raw_incls
       |> prep_decl ([], []) I raw_elems;
   in
-    lthy' |> Local_Theory.init_target
-      {background_naming = Local_Theory.background_naming_of lthy, after_close = after_close}
-      (Local_Theory.operations_of lthy)
+    lthy' |> Local_Theory.begin_target after_close
   end;
 
 in
diff -r 86f8fcdcff4a -r 7e0e497dacbc src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sat Oct 10 22:06:17 2020 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sat Oct 10 18:43:07 2020 +0000
@@ -73,9 +73,7 @@
   val exit_global: local_theory -> theory
   val exit_result: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * Proof.context
   val exit_result_global: (morphism -> 'a -> 'b) -> 'a * local_theory -> 'b * theory
-  val init_target: {background_naming: Name_Space.naming, after_close: local_theory -> local_theory} ->
-    operations -> local_theory -> Binding.scope * local_theory
-  val begin_target: local_theory -> Binding.scope * local_theory
+  val begin_target: (local_theory -> local_theory) -> local_theory -> Binding.scope * local_theory
   val open_target: local_theory -> local_theory
   val close_target: local_theory -> local_theory
   val subtarget: (local_theory -> local_theory) -> local_theory -> local_theory
@@ -394,11 +392,11 @@
     val lthy' = Data.map (cons entry) target;
   in (scope, lthy') end;
 
-fun begin_target lthy =
-  init_target {background_naming = background_naming_of lthy, after_close = I}
+fun begin_target after_close lthy =
+  init_target {background_naming = background_naming_of lthy, after_close = after_close}
     (operations_of lthy) lthy;
 
-val open_target = begin_target #> #2;
+val open_target = begin_target I #> #2;
 
 fun close_target lthy =
   let