1.1 --- a/src/Pure/PIDE/document.ML	Sat Jul 02 19:22:06 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sat Jul 02 20:22:02 2011 +0200
     1.3 @@ -80,10 +80,10 @@
     1.4      NONE => entries
     1.5    | SOME next => Entries.update (next, NONE) entries);
     1.6  
     1.7 -fun edit_node (hook, SOME id2) (Node entries) =
     1.8 -      Node (Entries.insert_after hook (id2, NONE) entries)
     1.9 -  | edit_node (hook, NONE) (Node entries) =
    1.10 -      Node (entries |> Entries.delete_after hook |> reset_after hook);
    1.11 +fun edit_node (id, SOME id2) (Node entries) =
    1.12 +      Node (Entries.insert_after id (id2, NONE) entries)
    1.13 +  | edit_node (id, NONE) (Node entries) =
    1.14 +      Node (entries |> Entries.delete_after id |> reset_after id);
    1.15  
    1.16  
    1.17  (* version operations *)