tuned;
authorwenzelm
Sat Feb 17 15:17:17 2018 +0100 (16 months ago ago)
changeset 676413eb12473a8bd
parent 67640 c89270d67169
child 67642 10ff1f077119
tuned;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Feb 17 12:58:07 2018 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Feb 17 15:17:17 2018 +0100
     1.3 @@ -279,8 +279,8 @@
     1.4        exit_transaction state
     1.5    | apply_tr int (Keep f) state =
     1.6        Runtime.controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state
     1.7 -  | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
     1.8 -      apply_transaction (fn x => f int x) g state
     1.9 +  | apply_tr int (Transaction (f, g)) (State (SOME node, _)) =
    1.10 +      apply_transaction (fn x => f int x) g node
    1.11    | apply_tr _ _ _ = raise UNDEF;
    1.12  
    1.13  fun apply_union _ [] state = raise FAILURE (state, UNDEF)