# HG changeset patch
# User wenzelm
# Date 1313876130 -7200
# Node ID 700008399ee5074279b930007936155def810870
# Parent  d453faed48158e563987aa68cc5781c91ae7d26b
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;

diff -r d453faed4815 -r 700008399ee5 src/HOL/Tools/Function/context_tree.ML
--- a/src/HOL/Tools/Function/context_tree.ML	Sat Aug 20 22:46:19 2011 +0200
+++ b/src/HOL/Tools/Function/context_tree.ML	Sat Aug 20 23:35:30 2011 +0200
@@ -205,7 +205,7 @@
         SOME _ => (T, x)
       | NONE =>
         let
-          val (T', x') = fold fill_table (Int_Graph.imm_succs G i) (T, x)
+          val (T', x') = Int_Graph.Keys.fold fill_table (Int_Graph.imm_succs G i) (T, x)
           val (v, x'') = f (the o Inttab.lookup T') i x'
         in
           (Inttab.update (i, v) T', x'')
@@ -226,7 +226,7 @@
             fun sub_step lu i x =
               let
                 val (ctxt', subtree) = nth branches i
-                val used = fold_rev (append o lu) (Int_Graph.imm_succs deps i) u
+                val used = Int_Graph.Keys.fold_rev (append o lu) (Int_Graph.imm_succs deps i) u
                 val (subs, x') = traverse_help (compose ctxt ctxt') subtree used x
                 val exported_subs = map (apfst (compose ctxt')) subs (* FIXME: Right order of composition? *)
               in
@@ -264,7 +264,7 @@
           fun sub_step lu i x =
             let
               val ((fixes, assumes), st) = nth branches i
-              val used = map lu (Int_Graph.imm_succs deps i)
+              val used = map lu (Int_Graph.immediate_succs deps i)
                 |> map (fn u_eq => (u_eq RS sym) RS eq_reflection)
                 |> filter_out Thm.is_reflexive
 
diff -r d453faed4815 -r 700008399ee5 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Aug 20 22:46:19 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Aug 20 23:35:30 2011 +0200
@@ -303,7 +303,7 @@
     val mapping = Termtab.empty |> fold (fn consts => fold (fn const =>
       Termtab.update (const, consts)) consts) constss;
     fun succs consts = consts
-      |> maps (Term_Graph.imm_succs gr)
+      |> maps (Term_Graph.immediate_succs gr)
       |> subtract eq_cname consts
       |> map (the o Termtab.lookup mapping)
       |> distinct (eq_list eq_cname);
diff -r d453faed4815 -r 700008399ee5 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Sat Aug 20 22:46:19 2011 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Sat Aug 20 23:35:30 2011 +0200
@@ -211,9 +211,11 @@
 
 (* job status *)
 
-fun ready_job task (Job list, ([], _)) = SOME (task, rev list)
-  | ready_job task (Passive abort, ([], _)) =
-      if is_canceled (group_of_task task) then SOME (task, [fn _ => abort ()])
+fun ready_job task (Job list, (deps, _)) =
+      if Task_Graph.Keys.is_empty deps then SOME (task, rev list) else NONE
+  | ready_job task (Passive abort, (deps, _)) =
+      if Task_Graph.Keys.is_empty deps andalso is_canceled (group_of_task task)
+      then SOME (task, [fn _ => abort ()])
       else NONE
   | ready_job _ _ = NONE;
 
@@ -232,7 +234,7 @@
     val (x, y, z, w) =
       Task_Graph.fold (fn (_, (job, (deps, _))) => fn (x, y, z, w) =>
           (case job of
-            Job _ => if null deps then (x + 1, y, z, w) else (x, y + 1, z, w)
+            Job _ => if Task_Graph.Keys.is_empty deps then (x + 1, y, z, w) else (x, y + 1, z, w)
           | Running _ => (x, y, z + 1, w)
           | Passive _ => (x, y, z, w + 1)))
         jobs (0, 0, 0, 0);
@@ -278,7 +280,7 @@
     val group = group_of_task task;
     val groups' = fold_groups (fn g => del_task (group_id g, task)) group groups;
     val jobs' = Task_Graph.del_node task jobs;
-    val maximal = null (Task_Graph.imm_succs jobs task);
+    val maximal = Task_Graph.is_maximal jobs task;
   in (maximal, make_queue groups' jobs') end;
 
 
@@ -342,7 +344,7 @@
           else
             let val entry as (_, (ds, _)) = #2 (Task_Graph.get_entry jobs task) in
               (case ready_job task entry of
-                NONE => ready_dep (Tasks.update (task, ()) seen) (ds @ tasks)
+                NONE => ready_dep (Tasks.update (task, ()) seen) (Task_Graph.Keys.dest ds @ tasks)
               | some => some)
             end;
 
diff -r d453faed4815 -r 700008399ee5 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Sat Aug 20 22:46:19 2011 +0200
+++ b/src/Pure/General/graph.ML	Sat Aug 20 23:35:30 2011 +0200
@@ -7,6 +7,14 @@
 signature GRAPH =
 sig
   type key
+  structure Keys:
+  sig
+    type T
+    val is_empty: T -> bool
+    val fold: (key -> 'a -> 'a) -> T -> 'a -> 'a
+    val fold_rev: (key -> 'a -> 'a) -> T -> 'a -> 'a
+    val dest: T -> key list
+  end
   type 'a T
   exception DUP of key
   exception SAME
@@ -15,20 +23,24 @@
   val is_empty: 'a T -> bool
   val keys: 'a T -> key list
   val dest: 'a T -> (key * key list) list
-  val get_first: (key * ('a * (key list * key list)) -> 'b option) -> 'a T -> 'b option
-  val fold: (key * ('a * (key list * key list)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
-  val minimals: 'a T -> key list
-  val maximals: 'a T -> key list
+  val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T -> 'b option
+  val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
   val subgraph: (key -> bool) -> 'a T -> 'a T
-  val get_entry: 'a T -> key -> key * ('a * (key list * key list))    (*exception UNDEF*)
+  val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T))        (*exception UNDEF*)
   val map: (key -> 'a -> 'b) -> 'a T -> 'b T
   val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
   val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
   val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T
-  val imm_preds: 'a T -> key -> key list
-  val imm_succs: 'a T -> key -> key list
+  val imm_preds: 'a T -> key -> Keys.T
+  val imm_succs: 'a T -> key -> Keys.T
+  val immediate_preds: 'a T -> key -> key list
+  val immediate_succs: 'a T -> key -> key list
   val all_preds: 'a T -> key list -> key list
   val all_succs: 'a T -> key list -> key list
+  val minimals: 'a T -> key list
+  val maximals: 'a T -> key list
+  val is_minimal: 'a T -> key -> bool
+  val is_maximal: 'a T -> key -> bool
   val strong_conn: 'a T -> key list list
   val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
   val default_node: key * 'a -> 'a T -> 'a T
@@ -59,27 +71,38 @@
 (* keys *)
 
 type key = Key.key;
-
 val eq_key = is_equal o Key.ord;
 
-val member_key = member eq_key;
-val remove_key = remove eq_key;
+structure Table = Table(Key);
+
+structure Keys =
+struct
 
+abstype T = Keys of unit Table.table
+with
 
-(* tables and sets of keys *)
+val empty = Keys Table.empty;
+fun is_empty (Keys tab) = Table.is_empty tab;
 
-structure Table = Table(Key);
-type keys = unit Table.table;
+fun member (Keys tab) = Table.defined tab;
+fun insert x (Keys tab) = Keys (Table.insert (K true) (x, ()) tab);
+fun remove x (Keys tab) = Keys (Table.delete_safe x tab);
+
+fun fold f (Keys tab) = Table.fold (f o #1) tab;
+fun fold_rev f (Keys tab) = Table.fold_rev (f o #1) tab;
 
-val empty_keys = Table.empty: keys;
+fun make xs = Basics.fold insert xs empty;
+fun dest keys = fold_rev cons keys [];
 
-fun member_keys tab = Table.defined (tab: keys);
-fun insert_keys x tab = Table.insert (K true) (x, ()) (tab: keys);
+fun filter P keys = fold (fn x => P x ? insert x) keys empty;
+
+end;
+end;
 
 
 (* graphs *)
 
-datatype 'a T = Graph of ('a * (key list * key list)) Table.table;
+datatype 'a T = Graph of ('a * (Keys.T * Keys.T)) Table.table;
 
 exception DUP = Table.DUP;
 exception UNDEF = Table.UNDEF;
@@ -88,18 +111,16 @@
 val empty = Graph Table.empty;
 fun is_empty (Graph tab) = Table.is_empty tab;
 fun keys (Graph tab) = Table.keys tab;
-fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, succs)) (Table.dest tab);
+fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, Keys.dest succs)) (Table.dest tab);
 
 fun get_first f (Graph tab) = Table.get_first f tab;
 fun fold_graph f (Graph tab) = Table.fold f tab;
 
-fun minimals G = fold_graph (fn (m, (_, ([], _))) => cons m | _ => I) G [];
-fun maximals G = fold_graph (fn (m, (_, (_, []))) => cons m | _ => I) G [];
-
 fun subgraph P G =
   let
     fun subg (k, (i, (preds, succs))) =
-      if P k then Table.update (k, (i, (filter P preds, filter P succs))) else I;
+      if P k then Table.update (k, (i, (Keys.filter P preds, Keys.filter P succs)))
+      else I;
   in Graph (fold_graph subg G Table.empty) end;
 
 fun get_entry (Graph tab) x =
@@ -132,20 +153,29 @@
 fun reachable next xs =
   let
     fun reach x (rs, R) =
-      if member_keys R x then (rs, R)
-      else fold reach (next x) (rs, insert_keys x R) |>> cons x;
+      if Keys.member R x then (rs, R)
+      else Keys.fold reach (next x) (rs, Keys.insert x R) |>> cons x;
     fun reachs x (rss, R) =
       reach x ([], R) |>> (fn rs => rs :: rss);
-  in fold reachs xs ([], empty_keys) end;
+  in fold reachs xs ([], Keys.empty) end;
 
 (*immediate*)
 fun imm_preds G = #1 o #2 o #2 o get_entry G;
 fun imm_succs G = #2 o #2 o #2 o get_entry G;
 
+fun immediate_preds G = Keys.dest o imm_preds G;
+fun immediate_succs G = Keys.dest o imm_succs G;
+
 (*transitive*)
 fun all_preds G = flat o #1 o reachable (imm_preds G);
 fun all_succs G = flat o #1 o reachable (imm_succs G);
 
+(*minimal and maximal elements*)
+fun minimals G = fold_graph (fn (m, (_, (preds, _))) => Keys.is_empty preds ? cons m) G [];
+fun maximals G = fold_graph (fn (m, (_, (_, succs))) => Keys.is_empty succs ? cons m) G [];
+fun is_minimal G x = Keys.is_empty (imm_preds G x);
+fun is_maximal G x = Keys.is_empty (imm_succs G x);
+
 (*strongly connected components; see: David King and John Launchbury,
   "Structuring Depth First Search Algorithms in Haskell"*)
 fun strong_conn G =
@@ -155,43 +185,44 @@
 (* nodes *)
 
 fun new_node (x, info) (Graph tab) =
-  Graph (Table.update_new (x, (info, ([], []))) tab);
+  Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab);
 
 fun default_node (x, info) (Graph tab) =
-  Graph (Table.default (x, (info, ([], []))) tab);
+  Graph (Table.default (x, (info, (Keys.empty, Keys.empty))) tab);
 
 fun del_nodes xs (Graph tab) =
   Graph (tab
     |> fold Table.delete xs
     |> Table.map (fn _ => fn (i, (preds, succs)) =>
-      (i, (fold remove_key xs preds, fold remove_key xs succs))));
+      (i, (fold Keys.remove xs preds, fold Keys.remove xs succs))));
 
 fun del_node x (G as Graph tab) =
   let
-    fun del_adjacent which y = Table.map_entry y (fn (i, ps) => (i, (which (remove_key x) ps)));
+    fun del_adjacent which y =
+      Table.map_entry y (fn (i, ps) => (i, (which (Keys.remove x) ps)));
     val (preds, succs) = #2 (#2 (get_entry G x));
   in
     Graph (tab
       |> Table.delete x
-      |> fold (del_adjacent apsnd) preds
-      |> fold (del_adjacent apfst) succs)
+      |> Keys.fold (del_adjacent apsnd) preds
+      |> Keys.fold (del_adjacent apfst) succs)
   end;
 
 
 (* edges *)
 
-fun is_edge G (x, y) = member_key (imm_succs G x) y handle UNDEF _ => false;
+fun is_edge G (x, y) = Keys.member (imm_succs G x) y handle UNDEF _ => false;
 
 fun add_edge (x, y) G =
   if is_edge G (x, y) then G
   else
-    G |> map_entry y (fn (i, (preds, succs)) => (i, (x :: preds, succs)))
-      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, y :: succs)));
+    G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.insert x preds, succs)))
+      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.insert y succs)));
 
 fun del_edge (x, y) G =
   if is_edge G (x, y) then
-    G |> map_entry y (fn (i, (preds, succs)) => (i, (remove_key x preds, succs)))
-      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, remove_key y succs)))
+    G |> map_entry y (fn (i, (preds, succs)) => (i, (Keys.remove x preds, succs)))
+      |> map_entry x (fn (i, (preds, succs)) => (i, (preds, Keys.remove y succs)))
   else G;
 
 fun diff_edges G1 G2 =
@@ -203,7 +234,7 @@
 
 (* join and merge *)
 
-fun no_edges (i, _) = (i, ([], []));
+fun no_edges (i, _) = (i, (Keys.empty, Keys.empty));
 
 fun join f (G1 as Graph tab1, G2 as Graph tab2) =
   let fun join_node key ((i1, edges1), (i2, _)) = (f key (i1, i2), edges1) in
@@ -227,11 +258,11 @@
     fun red x x' = is_edge G (x, x') andalso not (eq_key (x', z));
     fun irreds [] xs' = xs'
       | irreds (x :: xs) xs' =
-          if not (member_keys X x) orelse eq_key (x, z) orelse member_key path x orelse
+          if not (Keys.member X x) orelse eq_key (x, z) orelse member eq_key path x orelse
             exists (red x) xs orelse exists (red x) xs'
           then irreds xs xs'
           else irreds xs (x :: xs');
-  in irreds (imm_preds G z) [] end;
+  in irreds (immediate_preds G z) [] end;
 
 fun irreducible_paths G (x, y) =
   let
@@ -249,8 +280,8 @@
     val (_, X) = reachable (imm_succs G) [x];
     fun paths path z =
       if not (null path) andalso eq_key (x, z) then [z :: path]
-      else if member_keys X z andalso not (member_key path z)
-      then maps (paths (z :: path)) (imm_preds G z)
+      else if Keys.member X z andalso not (member eq_key path z)
+      then maps (paths (z :: path)) (immediate_preds G z)
       else [];
   in paths [] y end;
 
@@ -297,7 +328,7 @@
     val results = (xs, Table.empty) |-> fold (fn x => fn tab =>
       let
         val a = get_node G x;
-        val deps = imm_preds G x |> map (fn y =>
+        val deps = immediate_preds G x |> map (fn y =>
           (case Table.lookup tab y of
             SOME b => (y, b)
           | NONE => raise DEP (x, y)));
diff -r d453faed4815 -r 700008399ee5 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Aug 20 22:46:19 2011 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Aug 20 23:35:30 2011 +0200
@@ -407,7 +407,7 @@
     val {classes = (space, algebra), ...} = Type.rep_tsig (Proof_Context.tsig_of ctxt);
     val classes = Sorts.classes_of algebra;
     fun entry (c, (i, (_, cs))) =
-      (i, {name = Name_Space.extern ctxt space c, ID = c, parents = cs,
+      (i, {name = Name_Space.extern ctxt space c, ID = c, parents = Graph.Keys.dest cs,
             dir = "", unfold = true, path = ""});
     val gr =
       Graph.fold (cons o entry) classes []
diff -r d453faed4815 -r 700008399ee5 src/Pure/PIDE/document.ML
--- 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);
diff -r d453faed4815 -r 700008399ee5 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat Aug 20 22:46:19 2011 +0200
+++ b/src/Pure/axclass.ML	Sat Aug 20 23:35:30 2011 +0200
@@ -220,7 +220,9 @@
       in ((c1_pred, c2_succ), th') end;
 
     val new_classrels =
-      Library.map_product pair (c1 :: Graph.imm_preds classes c1) (c2 :: Graph.imm_succs classes c2)
+      Library.map_product pair
+        (c1 :: Graph.immediate_preds classes c1)
+        (c2 :: Graph.immediate_succs classes c2)
       |> filter_out ((op =) orf Symreltab.defined classrels)
       |> map gen_classrel;
     val needed = not (null new_classrels);
diff -r d453faed4815 -r 700008399ee5 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Sat Aug 20 22:46:19 2011 +0200
+++ b/src/Pure/sorts.ML	Sat Aug 20 23:35:30 2011 +0200
@@ -128,7 +128,7 @@
 
 fun all_classes (Algebra {classes, ...}) = Graph.all_preds classes (Graph.maximals classes);
 
-val super_classes = Graph.imm_succs o classes_of;
+val super_classes = Graph.immediate_succs o classes_of;
 
 
 (* class relations *)
@@ -413,7 +413,7 @@
       end;
 
     fun derive (_, []) = []
-      | derive (T as Type (a, Us), S) =
+      | derive (Type (a, Us), S) =
           let
             val Ss = mg_domain algebra a S;
             val dom = map2 (fn U => fn S => derive (U, S) ~~ S) Us Ss;
diff -r d453faed4815 -r 700008399ee5 src/Tools/Code/code_namespace.ML
--- a/src/Tools/Code/code_namespace.ML	Sat Aug 20 22:46:19 2011 +0200
+++ b/src/Tools/Code/code_namespace.ML	Sat Aug 20 23:35:30 2011 +0200
@@ -86,7 +86,8 @@
       end;
     val proto_program = Graph.empty
       |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
-      |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
+      |> Graph.fold (fn (name, (_, (_, names))) =>
+          Graph.Keys.fold (add_dependency name) names) program;
 
     (* name declarations and statement modifications *)
     fun declare name (base, stmt) (gr, nsp) = 
@@ -191,7 +192,8 @@
       in (map_module name_fragments_common o apsnd) add_edge end;
     val proto_program = empty_program
       |> Graph.fold (fn (name, (stmt, _)) => add_stmt name stmt) program
-      |> Graph.fold (fn (name, (_, (_, names))) => fold (add_dependency name) names) program;
+      |> Graph.fold (fn (name, (_, (_, names))) =>
+          Graph.Keys.fold (add_dependency name) names) program;
 
     (* name declarations, data and statement modifications *)
     fun make_declarations nsps (data, nodes) =
diff -r d453faed4815 -r 700008399ee5 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Sat Aug 20 22:46:19 2011 +0200
+++ b/src/Tools/Code/code_preproc.ML	Sat Aug 20 23:35:30 2011 +0200
@@ -309,7 +309,7 @@
     val diff_classes = new_classes |> subtract (op =) old_classes;
   in if null diff_classes then vardeps_data
   else let
-    val c_ks = Vargraph.imm_succs (fst vardeps_data) c_k |> insert (op =) c_k;
+    val c_ks = Vargraph.immediate_succs (fst vardeps_data) c_k |> insert (op =) c_k;
   in
     vardeps_data
     |> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes)
diff -r d453faed4815 -r 700008399ee5 src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Sat Aug 20 22:46:19 2011 +0200
+++ b/src/Tools/Code/code_scala.ML	Sat Aug 20 23:35:30 2011 +0200
@@ -321,7 +321,7 @@
          of Code_Thingol.Classinst _ => true
           | _ => false;
         val implicits = filter (is_classinst o Graph.get_node program)
-          (Graph.imm_succs program name);
+          (Graph.immediate_succs program name);
       in union (op =) implicits end;
     fun modify_stmt (_, Code_Thingol.Fun (_, (_, SOME _))) = NONE
       | modify_stmt (_, Code_Thingol.Datatypecons _) = NONE
diff -r d453faed4815 -r 700008399ee5 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sat Aug 20 22:46:19 2011 +0200
+++ b/src/Tools/Code/code_thingol.ML	Sat Aug 20 23:35:30 2011 +0200
@@ -921,7 +921,7 @@
       let
         val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
           Graph.get_node program1 Term.dummy_patternN;
-        val deps = Graph.imm_succs program1 Term.dummy_patternN;
+        val deps = Graph.immediate_succs program1 Term.dummy_patternN;
         val program2 = Graph.del_nodes [Term.dummy_patternN] program1;
         val deps_all = Graph.all_succs program2 deps;
         val program3 = Graph.subgraph (member (op =) deps_all) program2;
@@ -1010,7 +1010,7 @@
     val mapping = Symtab.empty |> fold (fn consts => fold (fn const =>
       Symtab.update (const, consts)) consts) constss;
     fun succs consts = consts
-      |> maps (Graph.imm_succs eqngr)
+      |> maps (Graph.immediate_succs eqngr)
       |> subtract (op =) consts
       |> map (the o Symtab.lookup mapping)
       |> distinct (op =);
diff -r d453faed4815 -r 700008399ee5 src/Tools/codegen.ML
--- a/src/Tools/codegen.ML	Sat Aug 20 22:46:19 2011 +0200
+++ b/src/Tools/codegen.ML	Sat Aug 20 23:35:30 2011 +0200
@@ -756,7 +756,7 @@
           let val SOME (x, y) = get_first (fn (x, (_, a', _)) =>
             if a = a' then Option.map (pair x)
               (find_first ((fn (_, b', _) => b' = b) o Graph.get_node gr)
-                (Graph.imm_succs gr x))
+                (Graph.immediate_succs gr x))
             else NONE) code
           in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end
       | string_of_cycle _ = ""
@@ -767,7 +767,7 @@
         val mod_gr = fold_rev Graph.add_edge_acyclic
           (maps (fn (s, (_, module, _)) => map (pair module)
             (filter_out (fn s => s = module) (map (#2 o Graph.get_node gr)
-              (Graph.imm_succs gr s)))) code)
+              (Graph.immediate_succs gr s)))) code)
           (fold_rev (Graph.new_node o rpair ()) modules Graph.empty);
         val modules' =
           rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs))
diff -r d453faed4815 -r 700008399ee5 src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Sat Aug 20 22:46:19 2011 +0200
+++ b/src/Tools/nbe.ML	Sat Aug 20 23:35:30 2011 +0200
@@ -471,7 +471,7 @@
       then (nbe_program, (maxidx, idx_tab))
       else (nbe_program, (maxidx, idx_tab))
         |> compile_stmts thy (map (fn name => ((name, Graph.get_node program name),
-          Graph.imm_succs program name)) names);
+          Graph.immediate_succs program name)) names);
   in
     fold_rev add_stmts (Graph.strong_conn program)
   end;
diff -r d453faed4815 -r 700008399ee5 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Sat Aug 20 22:46:19 2011 +0200
+++ b/src/Tools/subtyping.ML	Sat Aug 20 23:35:30 2011 +0200
@@ -171,10 +171,10 @@
 fun get_succs G T = Typ_Graph.all_succs G [T];
 fun maybe_new_typnode T G = perhaps (try (Typ_Graph.new_node (T, ()))) G;
 fun maybe_new_typnodes Ts G = fold maybe_new_typnode Ts G;
-fun new_imm_preds G Ts =
-  subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.imm_preds G) Ts));
-fun new_imm_succs G Ts =
-  subtract op= Ts (distinct (op =) (maps (Typ_Graph.imm_succs G) Ts));
+fun new_imm_preds G Ts =  (* FIXME inefficient *)
+  subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.immediate_preds G) Ts));
+fun new_imm_succs G Ts =  (* FIXME inefficient *)
+  subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.immediate_succs G) Ts));
 
 
 (* Graph shortcuts *)
@@ -406,7 +406,7 @@
     (*styps stands either for supertypes or for subtypes of a type T
       in terms of the subtype-relation (excluding T itself)*)
     fun styps super T =
-      (if super then Graph.imm_succs else Graph.imm_preds) coes_graph T
+      (if super then Graph.immediate_succs else Graph.immediate_preds) coes_graph T
         handle Graph.UNDEF _ => [];
 
     fun minmax sup (T :: Ts) =