--- a/src/Pure/PIDE/document.ML Sat Aug 20 22:46:19 2011 +0200
+++ b/src/Pure/PIDE/document.ML Sat Aug 20 23:35:30 2011 +0200
@@ -145,7 +145,8 @@
|> default_node name
|> fold default_node parents;
val nodes2 = nodes1
- |> fold (fn dep => Graph.del_edge (dep, name)) (Graph.imm_preds nodes1 name);
+ |> 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)
handle Graph.CYCLES cs => (Exn.Exn (ERROR (cat_lines (map cycle_msg cs))), nodes2);