--- a/src/Pure/Isar/target_context.ML Sat Oct 24 14:40:12 2020 +0000
+++ b/src/Pure/Isar/target_context.ML Sat Oct 24 15:16:54 2020 +0000
@@ -7,7 +7,7 @@
signature TARGET_CONTEXT =
sig
val context_begin_named_cmd: xstring * Position.T -> theory -> local_theory
- val end_named_cmd: local_theory -> theory
+ val end_named_cmd: local_theory -> Context.generic
val switch_named_cmd: (xstring * Position.T) option -> Context.generic ->
(local_theory -> Context.generic) * local_theory
val context_begin_nested_cmd: (xstring * Position.T) list -> Element.context list ->
@@ -21,17 +21,17 @@
fun context_begin_named_cmd ("-", _) thy = Named_Target.theory_init thy
| context_begin_named_cmd target thy = Named_Target.init (Locale.check thy target) thy;
-val end_named_cmd = Local_Theory.exit_global;
+val end_named_cmd = Context.Theory o Local_Theory.exit_global;
fun switch_named_cmd NONE (Context.Theory thy) =
- (Context.Theory o end_named_cmd, Named_Target.theory_init thy)
+ (Context.Theory o Local_Theory.exit_global, Named_Target.theory_init thy)
| switch_named_cmd (SOME name) (Context.Theory thy) =
- (Context.Theory o end_named_cmd, context_begin_named_cmd name thy)
+ (Context.Theory o Local_Theory.exit_global, context_begin_named_cmd name thy)
| switch_named_cmd NONE (Context.Proof lthy) =
(Context.Proof o Local_Theory.reset, lthy)
| switch_named_cmd (SOME name) (Context.Proof lthy) =
- (Context.Proof o Named_Target.reinit lthy o end_named_cmd,
- (context_begin_named_cmd name o end_named_cmd o Local_Theory.assert_nonbrittle) lthy);
+ (Context.Proof o Named_Target.reinit lthy o Local_Theory.exit_global,
+ (context_begin_named_cmd name o Local_Theory.exit_global_nonbrittle) lthy);
fun includes raw_incls lthy =
Bundle.includes (map (Bundle.check lthy) raw_incls) lthy;
@@ -45,10 +45,14 @@
|> Local_Theory.begin_nested
|> snd;
-fun end_nested_cmd lthy =
- if Named_Target.is_theory lthy
- then Context.Theory (Local_Theory.exit_global lthy)
- else Context.Proof lthy;
+fun end_nested_cmd lthy =
+ let
+ val lthy' = Local_Theory.end_nested lthy
+ in
+ if Named_Target.is_theory lthy'
+ then Context.Theory (Local_Theory.exit_global lthy')
+ else Context.Proof lthy'
+ end;
end;