# HG changeset patch
# User wenzelm
# Date 1116852996 -7200
# Node ID 7d68cd1b1b8b7710012a3d71f231d2b24dcf12e0
# Parent  6e2c020eed45bade71584a8f54334199d90ca344
node_trans: revert to original transaction code (pre 1.54);

diff -r 6e2c020eed45 -r 7d68cd1b1b8b src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon May 23 14:56:35 2005 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon May 23 14:56:36 2005 +0200
@@ -215,14 +215,15 @@
       let
         fun mk_state nd = State (SOME (nd, term));
 
-        val f' = checkpoint_node int o f int o copy_node int;
+        val cont_node = History.map (checkpoint_node int) node;
+        val back_node = History.map (copy_node int) cont_node;
 
-        val trans = if hist then History.apply else History.map;
+        val trans = if hist then History.apply_copy (copy_node int) else History.map;
         val (result, opt_exn) =
-          (mk_state (transform_error (interruptible (trans f')) node), NONE)
-            handle exn => (mk_state node, SOME exn);
+          (mk_state (transform_error (interruptible (trans (f int))) cont_node), NONE)
+            handle exn => (mk_state cont_node, SOME exn);
       in
-        if is_stale result then return (mk_state node, SOME (if_none opt_exn rollback))
+        if is_stale result then return (mk_state back_node, SOME (if_none opt_exn rollback))
         else return (result, opt_exn)
       end;