--- 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