diff -r ceb190f4f69f -r 301a721af68b src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Nov 22 20:54:26 2013 +0100
+++ b/src/Pure/PIDE/document.ML	Fri Nov 22 21:13:44 2013 +0100
@@ -11,7 +11,6 @@
   type node_header = string * Thy_Header.header * string list
   type overlay = Document_ID.command * (string * string list)
   datatype node_edit =
-    Clear |    (* FIXME unused !? *)
     Edits of (Document_ID.command option * Document_ID.command option) list |
     Deps of node_header |
     Perspective of bool * Document_ID.command list * overlay list
@@ -76,7 +75,6 @@
 val no_perspective = make_perspective (false, [], []);
 
 val empty_node = make_node (no_header, no_perspective, Entries.empty, NONE);
-val clear_node = map_node (fn (header, _, _, _) => (header, no_perspective, Entries.empty, NONE));
 
 
 (* basic components *)
@@ -145,7 +143,6 @@
 type overlay = Document_ID.command * (string * string list);
 
 datatype node_edit =
-  Clear |
   Edits of (Document_ID.command option * Document_ID.command option) list |
   Deps of node_header |
   Perspective of bool * Document_ID.command list * overlay list;
@@ -193,8 +190,7 @@
 fun edit_nodes (name, node_edit) (Version nodes) =
   Version
     (case node_edit of
-      Clear => update_node name clear_node nodes
-    | Edits edits => update_node name (edit_node edits) nodes
+      Edits edits => update_node name (edit_node edits) nodes
     | Deps (master, header, errors) =>
         let
           val imports = map fst (#imports header);