1.1 --- a/src/Pure/Isar/toplevel.ML	Tue Jul 05 11:45:48 2011 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Jul 05 19:45:59 2011 +0200
     1.3 @@ -185,7 +185,7 @@
     1.4      Proof (prf, _) => Proof_Node.position prf
     1.5    | _ => raise UNDEF);
     1.6  
     1.7 -fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = Theory.end_theory thy
     1.8 +fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
     1.9    | end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos);
    1.10  
    1.11  
    1.12 @@ -284,6 +284,12 @@
    1.13      | SOME exn => raise FAILURE (result', exn))
    1.14    end;
    1.15  
    1.16 +val exit_transaction =
    1.17 +  apply_transaction
    1.18 +    (fn Theory (Context.Theory thy, _) => Theory (Context.Theory (Theory.end_theory thy), NONE)
    1.19 +      | node => node) (K ())
    1.20 +  #> (fn State (node', _) => State (NONE, node'));
    1.21 +
    1.22  end;
    1.23  
    1.24  
    1.25 @@ -300,8 +306,8 @@
    1.26  fun apply_tr _ (Init (master, _, f)) (State (NONE, _)) =
    1.27        State (SOME (Theory (Context.Theory
    1.28            (Theory.checkpoint (Runtime.controlled_execution f master)), NONE)), NONE)
    1.29 -  | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _)), _)) =
    1.30 -      State (NONE, prev)
    1.31 +  | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
    1.32 +      exit_transaction state
    1.33    | apply_tr int (Keep f) state =
    1.34        Runtime.controlled_execution (fn x => tap (f int) x) state
    1.35    | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =