# HG changeset patch
# User wenzelm
# Date 1309887959 -7200
# Node ID 6d73cceb1503c3c7031dda6835cb5113d1deefd5
# Parent  7be2e51928cb6d392b56b07b63e436301ddfb28d
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
reduced Theory.end_theory to plain projection, outside transaction context (see also ddc3b72f9a42);

diff -r 7be2e51928cb -r 6d73cceb1503 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jul 05 11:45:48 2011 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 05 19:45:59 2011 +0200
@@ -185,7 +185,7 @@
     Proof (prf, _) => Proof_Node.position prf
   | _ => raise UNDEF);
 
-fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = Theory.end_theory thy
+fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
   | end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos);
 
 
@@ -284,6 +284,12 @@
     | SOME exn => raise FAILURE (result', exn))
   end;
 
+val exit_transaction =
+  apply_transaction
+    (fn Theory (Context.Theory thy, _) => Theory (Context.Theory (Theory.end_theory thy), NONE)
+      | node => node) (K ())
+  #> (fn State (node', _) => State (NONE, node'));
+
 end;
 
 
@@ -300,8 +306,8 @@
 fun apply_tr _ (Init (master, _, f)) (State (NONE, _)) =
       State (SOME (Theory (Context.Theory
           (Theory.checkpoint (Runtime.controlled_execution f master)), NONE)), NONE)
-  | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _)), _)) =
-      State (NONE, prev)
+  | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
+      exit_transaction state
   | apply_tr int (Keep f) state =
       Runtime.controlled_execution (fn x => tap (f int) x) state
   | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =