# HG changeset patch
# User wenzelm
# Date 918491510 -3600
# Node ID 6dc692fb3d281b71c8a3a365ffd621d0d0ed745e
# Parent  a8010d459ef7875982442762190ee46e2ee04a35
added fetch, fetch_theory;

diff -r a8010d459ef7 -r 6dc692fb3d28 src/Pure/context.ML
--- a/src/Pure/context.ML	Mon Feb 08 17:30:22 1999 +0100
+++ b/src/Pure/context.ML	Mon Feb 08 17:31:50 1999 +0100
@@ -18,6 +18,8 @@
   val set_context: theory option -> unit
   val reset_context: unit -> unit
   val setmp: theory option -> ('a -> 'b) -> 'a -> 'b
+  val fetch: theory option -> ('a -> 'b) -> 'a -> 'b * theory option
+  val fetch_theory: theory -> ('a -> 'b) -> 'a -> 'b * theory
   val save: ('a -> 'b) -> 'a -> 'b
   val >> : (theory -> theory) -> unit
 end;
@@ -44,6 +46,14 @@
 fun context thy = set_context (Some thy);
 fun reset_context () = set_context None;
 
+fun fetch opt_thy f x =
+  setmp opt_thy (fn x => let val y = f x in (y, get_context ()) end) x;
+
+fun fetch_theory thy f x =
+  (case fetch (Some thy) f x of
+    (y, Some thy') => (y, thy')
+  | (_, None) => error "Missing ML theory context");
+
 fun save f x = setmp (get_context ()) f x;