# HG changeset patch
# User wenzelm
# Date 1518877037 -3600
# Node ID 3eb12473a8bd0a97656ce3adac73d7bed7b2671e
# Parent  c89270d67169c40a02cb0a68f9a17fbde347fcdb
tuned;

diff -r c89270d67169 -r 3eb12473a8bd src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Feb 17 12:58:07 2018 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sat Feb 17 15:17:17 2018 +0100
@@ -279,8 +279,8 @@
       exit_transaction state
   | apply_tr int (Keep f) state =
       Runtime.controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state
-  | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
-      apply_transaction (fn x => f int x) g state
+  | apply_tr int (Transaction (f, g)) (State (SOME node, _)) =
+      apply_transaction (fn x => f int x) g node
   | apply_tr _ _ _ = raise UNDEF;
 
 fun apply_union _ [] state = raise FAILURE (state, UNDEF)