# HG changeset patch
# User wenzelm
# Date 1206558878 -3600
# Node ID 0cb6f2013e99500a2e79e4055da806717b5149ad
# Parent  56fd70fb75714b91395c81f6fc5756acde713f3c
removed obsolete pass, save;

diff -r 56fd70fb7571 -r 0cb6f2013e99 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed Mar 26 20:14:37 2008 +0100
+++ b/src/Pure/ML/ml_context.ML	Wed Mar 26 20:14:38 2008 +0100
@@ -20,9 +20,7 @@
   val setmp: Context.generic option -> ('a -> 'b) -> 'a -> 'b
   val the_generic_context: unit -> Context.generic
   val the_local_context: unit -> Proof.context
-  val pass: Context.generic option -> ('a -> 'b) -> 'a -> 'b * Context.generic option
   val pass_context: Context.generic -> ('a -> 'b) -> 'a -> 'b * Context.generic
-  val save: ('a -> 'b) -> 'a -> 'b
   val >> : (theory -> theory) -> unit
   val add_keywords: string list -> unit
   val inline_antiq: string ->
@@ -63,16 +61,11 @@
 
 val the_context = Context.theory_of o the_generic_context;
 
-fun pass opt_context f x =
-  setmp opt_context (fn x => let val y = f x in (y, get_context ()) end) x;
-
 fun pass_context context f x =
-  (case pass (SOME context) f x of
+  (case setmp (SOME context) (fn () => (f x, get_context ())) () of
     (y, SOME context') => (y, context')
   | (_, NONE) => error "Lost context in ML");
 
-fun save f x = NAMED_CRITICAL "ML" (fn () => setmp (get_context ()) f x);
-
 fun change_theory f = NAMED_CRITICAL "ML" (fn () =>
   set_context (SOME (Context.map_theory f (the_generic_context ()))));