--- a/src/Pure/Isar/named_target.ML Thu Jan 24 02:47:52 2019 +0000
+++ b/src/Pure/Isar/named_target.ML Wed Jan 23 17:54:50 2019 +0000
@@ -16,6 +16,8 @@
string -> theory -> local_theory
val theory_init: theory -> local_theory
val theory_map: (local_theory -> local_theory) -> theory -> theory
+ val theory_map_result: (morphism -> 'a -> 'b) -> (local_theory -> 'a * local_theory) ->
+ theory -> 'b * theory
val begin: xstring * Position.T -> theory -> local_theory
val exit: local_theory -> theory
val switch: (xstring * Position.T) option -> Context.generic ->
@@ -135,7 +137,9 @@
val theory_init = init "";
-fun theory_map f = theory_init #> f #> Local_Theory.exit_global;
+fun theory_map g = theory_init #> g #> Local_Theory.exit_global;
+
+fun theory_map_result f g = theory_init #> g #> Local_Theory.exit_result_global f;
(* toplevel interaction *)
--- a/src/Pure/Isar/typedecl.ML Thu Jan 24 02:47:52 2019 +0000
+++ b/src/Pure/Isar/typedecl.ML Wed Jan 23 17:54:50 2019 +0000
@@ -88,9 +88,7 @@
end;
fun typedecl_global {final} decl =
- Named_Target.theory_init
- #> typedecl {final = final} decl
- #> Local_Theory.exit_result_global Morphism.typ;
+ Named_Target.theory_map_result Morphism.typ (typedecl {final = final} decl);
(* type abbreviations *)
@@ -130,8 +128,6 @@
end;
fun abbrev_global decl rhs =
- Named_Target.theory_init
- #> abbrev decl rhs
- #> Local_Theory.exit_result_global (K I);
+ Named_Target.theory_map_result (K I) (abbrev decl rhs);
end;