# HG changeset patch
# User wenzelm
# Date 918244638 -3600
# Node ID bd7b4a23118f4beabad1c66d4d7ca0e6335fd4c4
# Parent  699b4daf14512b021cc34d1ff00469a50e38c647
setmp: theory option;
save;

diff -r 699b4daf1451 -r bd7b4a23118f src/Pure/context.ML
--- a/src/Pure/context.ML	Fri Feb 05 20:56:50 1999 +0100
+++ b/src/Pure/context.ML	Fri Feb 05 20:57:18 1999 +0100
@@ -17,7 +17,8 @@
   val get_context: unit -> theory option
   val set_context: theory option -> unit
   val reset_context: unit -> unit
-  val setmp: theory -> ('a -> 'b) -> 'a -> 'b
+  val setmp: theory option -> ('a -> 'b) -> 'a -> 'b
+  val save: ('a -> 'b) -> 'a -> 'b
   val >> : (theory -> theory) -> unit
 end;
 
@@ -32,7 +33,7 @@
 in
   fun get_context () = ! current_theory;
   fun set_context opt_thy = current_theory := opt_thy;
-  fun setmp thy f x = Library.setmp current_theory (Some thy) f x;
+  fun setmp opt_thy f x = Library.setmp current_theory opt_thy f x;
 end;
 
 fun the_context () =
@@ -43,6 +44,8 @@
 fun context thy = set_context (Some thy);
 fun reset_context () = set_context None;
 
+fun save f x = setmp (get_context ()) f x;
+
 
 (* map context *)