1.1 --- a/src/Pure/context.ML	Thu Mar 27 14:41:13 2008 +0100
     1.2 +++ b/src/Pure/context.ML	Thu Mar 27 14:41:14 2008 +0100
     1.3 @@ -22,7 +22,6 @@
     1.4    val parents_of: theory -> theory list
     1.5    val ancestors_of: theory -> theory list
     1.6    val is_stale: theory -> bool
     1.7 -  val ProtoPureN: string
     1.8    val PureN: string
     1.9    val CPureN: string
    1.10    val draftN: string
    1.11 @@ -43,7 +42,6 @@
    1.12    val copy_thy: theory -> theory
    1.13    val checkpoint_thy: theory -> theory
    1.14    val finish_thy: theory -> theory
    1.15 -  val pre_pure_thy: theory
    1.16    val begin_thy: (theory -> Pretty.pp) -> string -> theory list -> theory
    1.17    (*proof context*)
    1.18    type proof
    1.19 @@ -69,6 +67,7 @@
    1.20    val set_thread_data: generic option -> unit
    1.21    val setmp_thread_data: generic option -> ('a -> 'b) -> 'a -> 'b
    1.22    val >> : (theory -> theory) -> unit
    1.23 +  val >>> : (theory -> 'a * theory) -> 'a
    1.24    (*delayed setup*)
    1.25    val add_setup: (theory -> theory) -> unit
    1.26    val setup: unit -> theory -> theory
    1.27 @@ -198,7 +197,6 @@
    1.28  
    1.29  (* names *)
    1.30  
    1.31 -val ProtoPureN = "ProtoPure";
    1.32  val PureN = "Pure";
    1.33  val CPureN = "CPure";
    1.34  
    1.35 @@ -337,7 +335,7 @@
    1.36    in thy' end;
    1.37  
    1.38  val pre_pure_thy = create_thy draftN NONE (serial (), draftN) Inttab.empty Inttab.empty
    1.39 -  Datatab.empty (make_ancestry [] []) (make_history ProtoPureN 0 []);
    1.40 +  Datatab.empty (make_ancestry [] []) (make_history PureN 0 []);
    1.41  
    1.42  
    1.43  (* named theory nodes *)
    1.44 @@ -526,10 +524,18 @@
    1.45  fun set_thread_data context = Multithreading.put_data (tag, context);
    1.46  fun setmp_thread_data context = Library.setmp_thread_data tag (thread_data ()) context;
    1.47  
    1.48 +end;
    1.49 +
    1.50 +fun >>> f =
    1.51 +  let
    1.52 +    val (res, thy') = f (the_theory (the_thread_data ()));
    1.53 +    val _ = set_thread_data (SOME (Theory thy'));
    1.54 +  in res end;
    1.55 +
    1.56  nonfix >>;
    1.57 -fun >> f = set_thread_data (SOME (map_theory f (the_thread_data ())));
    1.58 +fun >> f = >>> (fn thy => ((), f thy));
    1.59  
    1.60 -end;
    1.61 +val _ = set_thread_data (SOME (Theory pre_pure_thy));
    1.62  
    1.63  
    1.64