# HG changeset patch
# User wenzelm
# Date 1216116794 -7200
# Node ID 69c00b56fb369b2bc3f9ceadac9ee8223484abf9
# Parent  86cf8f2493ca85c5d82b2563977358492f47c4ed
tuned;

diff -r 86cf8f2493ca -r 69c00b56fb36 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jul 15 11:50:04 2008 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 15 12:13:14 2008 +0200
@@ -168,7 +168,7 @@
 
 (* current node *)
 
-fun previous_node_of (State (_, prev_node)) = Option.map #1 prev_node;
+fun previous_node_of (State (_, prev)) = Option.map #1 prev;
 
 fun node_of (State (NONE, _)) = raise UNDEF
   | node_of (State (SOME (node, _), _)) = node;
@@ -367,8 +367,8 @@
 
 fun apply_tr int _ (Init (_, f, exit)) (State (NONE, _)) =
       State (SOME (Theory (Context.Theory (Theory.checkpoint (f int)), NONE), exit), NONE)
-  | apply_tr _ _ Exit (State (SOME (node as Theory (Context.Theory _, _), exit), _)) =
-      State (NONE, SOME (node, exit))
+  | apply_tr _ _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) =
+      State (NONE, prev)
   | apply_tr _ _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) =
       (controlled_execution exit thy; toplevel)
   | apply_tr int _ (Keep f) state =