# HG changeset patch
# User haftmann
# Date 1548266090 0
# Node ID 49d25343d3d431ced5f2b3b934a301ff01170938
# Parent  82750b732bb9a6cda369da91198d721117c987cc
combinator to lift local theory update to theory update

diff -r 82750b732bb9 -r 49d25343d3d4 src/Pure/Isar/named_target.ML
--- 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 *)
diff -r 82750b732bb9 -r 49d25343d3d4 src/Pure/Isar/typedecl.ML
--- 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;