src/Pure/context.ML
changeset 26463 9283b4185fdf
parent 26435 bdce320cd426
child 26486 b65a5272b360
     1.1 --- a/src/Pure/context.ML	Fri Mar 28 19:43:54 2008 +0100
     1.2 +++ b/src/Pure/context.ML	Fri Mar 28 20:02:04 2008 +0100
     1.3 @@ -66,8 +66,8 @@
     1.4    val the_thread_data: unit -> generic
     1.5    val set_thread_data: generic option -> unit
     1.6    val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
     1.7 -  val >> : (theory -> theory) -> unit
     1.8 -  val >>> : (theory -> 'a * theory) -> 'a
     1.9 +  val >> : (generic -> generic) -> unit
    1.10 +  val >>> : (generic -> 'a * generic) -> 'a
    1.11  end;
    1.12  
    1.13  signature PRIVATE_CONTEXT =
    1.14 @@ -525,12 +525,12 @@
    1.15  
    1.16  fun >>> f =
    1.17    let
    1.18 -    val (res, thy') = f (the_theory (the_thread_data ()));
    1.19 -    val _ = set_thread_data (SOME (Theory thy'));
    1.20 +    val (res, context') = f (the_thread_data ());
    1.21 +    val _ = set_thread_data (SOME context');
    1.22    in res end;
    1.23  
    1.24  nonfix >>;
    1.25 -fun >> f = >>> (fn thy => ((), f thy));
    1.26 +fun >> f = >>> (fn context => ((), f context));
    1.27  
    1.28  val _ = set_thread_data (SOME (Theory pre_pure_thy));
    1.29