tuned;
authorwenzelm
Tue Mar 09 12:05:07 1999 +0100 (1999-03-09)
changeset 6310353a8a9d9d2c
parent 6309 ca52347e259a
child 6311 15652e058e28
tuned;
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Tue Mar 09 11:09:01 1999 +0100
     1.2 +++ b/src/Pure/context.ML	Tue Mar 09 12:05:07 1999 +0100
     1.3 @@ -18,8 +18,8 @@
     1.4    val set_context: theory option -> unit
     1.5    val reset_context: unit -> unit
     1.6    val setmp: theory option -> ('a -> 'b) -> 'a -> 'b
     1.7 -  val fetch: theory option -> ('a -> 'b) -> 'a -> 'b * theory option
     1.8 -  val fetch_theory: theory -> ('a -> 'b) -> 'a -> 'b * theory
     1.9 +  val pass: theory option -> ('a -> 'b) -> 'a -> 'b * theory option
    1.10 +  val pass_theory: theory -> ('a -> 'b) -> 'a -> 'b * theory
    1.11    val save: ('a -> 'b) -> 'a -> 'b
    1.12    val >> : (theory -> theory) -> unit
    1.13  end;
    1.14 @@ -46,11 +46,11 @@
    1.15  fun context thy = set_context (Some thy);
    1.16  fun reset_context () = set_context None;
    1.17  
    1.18 -fun fetch opt_thy f x =
    1.19 +fun pass opt_thy f x =
    1.20    setmp opt_thy (fn x => let val y = f x in (y, get_context ()) end) x;
    1.21  
    1.22 -fun fetch_theory thy f x =
    1.23 -  (case fetch (Some thy) f x of
    1.24 +fun pass_theory thy f x =
    1.25 +  (case pass (Some thy) f x of
    1.26      (y, Some thy') => (y, thy')
    1.27    | (_, None) => error "Missing ML theory context");
    1.28