# HG changeset patch
# User berghofe
# Date 1109168340 -3600
# Node ID 14d1672598126114d09f5f19db53509d96d66ca1
# Parent  aea2f1706fdfc02751f74bf751735107cfbc541f
Modified node_trans to avoid duplication of signature stamps
when undoing.

diff -r aea2f1706fdf -r 14d167259812 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Feb 23 15:00:03 2005 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Feb 23 15:19:00 2005 +0100
@@ -214,15 +214,14 @@
       let
         fun mk_state nd = State (SOME (nd, term));
 
-        val cont_node = History.map (checkpoint_node int) node;
-        val back_node = History.map (copy_node int) cont_node;
+        val f' = checkpoint_node int o f int o copy_node int;
 
-        val trans = if hist then History.apply_copy (copy_node int) else History.map;
+        val trans = if hist then History.apply else History.map;
         val (result, opt_exn) =
-          (mk_state (transform_error (interruptible (trans (f int))) cont_node), NONE)
-            handle exn => (mk_state cont_node, SOME exn);
+          (mk_state (transform_error (interruptible (trans f')) node), NONE)
+            handle exn => (mk_state node, SOME exn);
       in
-        if is_stale result then return (mk_state back_node, SOME (if_none opt_exn rollback))
+        if is_stale result then return (mk_state node, SOME (if_none opt_exn rollback))
         else return (result, opt_exn)
       end;