# HG changeset patch
# User wenzelm
# Date 1309630922 -7200
# Node ID 9ef5479da29f24502d857149028c176172e4e471
# Parent  081e009549dce3e1edfcd172afc54566722e55b2
tuned;

diff -r 081e009549dc -r 9ef5479da29f src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Jul 02 19:22:06 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Sat Jul 02 20:22:02 2011 +0200
@@ -80,10 +80,10 @@
     NONE => entries
   | SOME next => Entries.update (next, NONE) entries);
 
-fun edit_node (hook, SOME id2) (Node entries) =
-      Node (Entries.insert_after hook (id2, NONE) entries)
-  | edit_node (hook, NONE) (Node entries) =
-      Node (entries |> Entries.delete_after hook |> reset_after hook);
+fun edit_node (id, SOME id2) (Node entries) =
+      Node (Entries.insert_after id (id2, NONE) entries)
+  | edit_node (id, NONE) (Node entries) =
+      Node (entries |> Entries.delete_after id |> reset_after id);
 
 
 (* version operations *)