tuned;
authorwenzelm
Sat, 17 Feb 2018 15:17:17 +0100
changeset 67641 3eb12473a8bd
parent 67640 c89270d67169
child 67642 10ff1f077119
tuned;
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)