src/Pure/Isar/named_target.ML

   val init: string -> theory -> local_theory
   val init': {setup: local_theory -> local_theory, conclude: local_theory -> local_theory} ->
     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 ->
     (local_theory -> Context.generic) * local_theory
 end;

 fun init ident thy =
   init' {setup = Data.put (SOME (target_of_ident thy ident)), conclude = I} ident thy;
 
 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 *)
 
 fun begin ("-", _) thy = theory_init thy