diff -r 1d2cbcc50fb2 -r 6024353549ca src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Wed Feb 29 23:31:35 2012 +0100
+++ b/src/Pure/PIDE/document.ML	Thu Mar 01 11:28:33 2012 +0100
@@ -212,15 +212,15 @@
         |> touch_node name
     | Header header =>
         let
-          val parents = (case header of Exn.Res (_, parents, _) => parents | _ => []);
+          val imports = (case header of Exn.Res (_, imports, _) => imports | _ => []);
           val nodes1 = nodes
             |> default_node name
-            |> fold default_node parents;
+            |> fold default_node imports;
           val nodes2 = nodes1
             |> Graph.Keys.fold
                 (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
           val (header', nodes3) =
-            (header, Graph.add_deps_acyclic (name, parents) nodes2)
+            (header, Graph.add_deps_acyclic (name, imports) nodes2)
               handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);
         in Graph.map_node name (set_header header') nodes3 end
         |> touch_node name