# HG changeset patch
# User wenzelm
# Date 1313926583 -7200
# Node ID b7f9e764532a110d9c7c17be2911e41e8a17e84b
# Parent  63cddfbc5a098a8ab5afc8b702c7340486ab140c# Parent  a93d25fb14fce9c5099c27f6b1b4d93e8056656f
merged

diff -r 63cddfbc5a09 -r b7f9e764532a Admin/polyml/future/ROOT.ML
--- a/Admin/polyml/future/ROOT.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/Admin/polyml/future/ROOT.ML	Sun Aug 21 13:36:23 2011 +0200
@@ -78,7 +78,6 @@
 use "General/table.ML";
 use "General/graph.ML";
 use "General/ord_list.ML";
-use "General/balanced_tree.ML";
 
 structure Position =
 struct
diff -r 63cddfbc5a09 -r b7f9e764532a src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/HOL/Library/Multiset.thy	Sun Aug 21 13:36:23 2011 +0200
@@ -1598,7 +1598,7 @@
 definition image_mset :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
   "image_mset f = fold_mset (op + o single o f) {#}"
 
-interpretation image_fun_commute: comp_fun_commute "op + o single o f"
+interpretation image_fun_commute: comp_fun_commute "op + o single o f" for f
 proof qed (simp add: add_ac fun_eq_iff)
 
 lemma image_mset_empty [simp]: "image_mset f {#} = {#}"
diff -r 63cddfbc5a09 -r b7f9e764532a src/HOL/Tools/Function/context_tree.ML
--- a/src/HOL/Tools/Function/context_tree.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/HOL/Tools/Function/context_tree.ML	Sun Aug 21 13:36:23 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 63cddfbc5a09 -r b7f9e764532a src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Sun Aug 21 13:36:23 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 63cddfbc5a09 -r b7f9e764532a src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/Concurrent/future.ML	Sun Aug 21 13:36:23 2011 +0200
@@ -62,12 +62,13 @@
   val fork: (unit -> 'a) -> 'a future
   val join_results: 'a future list -> 'a Exn.result list
   val join_result: 'a future -> 'a Exn.result
+  val joins: 'a future list -> 'a list
   val join: 'a future -> 'a
   val join_tasks: task list -> unit
   val value_result: 'a Exn.result -> 'a future
   val value: 'a -> 'a future
+  val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
   val map: ('a -> 'b) -> 'a future -> 'b future
-  val cond_forks: fork_params -> (unit -> 'a) list -> 'a future list
   val promise_group: group -> (unit -> unit) -> 'a future
   val promise: (unit -> unit) -> 'a future
   val fulfill_result: 'a future -> 'a Exn.result -> unit
@@ -185,13 +186,21 @@
 (* cancellation primitives *)
 
 fun cancel_now group = (*requires SYNCHRONIZED*)
-  Task_Queue.cancel (! queue) group;
+  let
+    val (tasks, threads) = Task_Queue.cancel (! queue) group;
+    val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
+  in tasks end;
+
+fun cancel_all () = (*requires SYNCHRONIZED*)
+  let
+    val (groups, threads) = Task_Queue.cancel_all (! queue);
+    val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
+  in groups end;
 
 fun cancel_later group = (*requires SYNCHRONIZED*)
  (Unsynchronized.change canceled (insert Task_Queue.eq_group group);
   broadcast scheduler_event);
 
-
 fun interruptible_task f x =
   (if Multithreading.available then
     Multithreading.with_attributes
@@ -379,7 +388,7 @@
   handle exn =>
     if Exn.is_interrupt exn then
      (Multithreading.tracing 1 (fn () => "Interrupt");
-      List.app cancel_later (Task_Queue.cancel_all (! queue));
+      List.app cancel_later (cancel_all ());
       broadcast_work (); true)
     else reraise exn;
 
@@ -534,6 +543,7 @@
 end;
 
 fun join_result x = singleton join_results x;
+fun joins xs = Par_Exn.release_all (join_results xs);
 fun join x = Exn.release (join_result x);
 
 fun join_tasks [] = ()
@@ -556,6 +566,10 @@
 
 fun value x = value_result (Exn.Res x);
 
+fun cond_forks args es =
+  if Multithreading.enabled () then forks args es
+  else map (fn e => value_result (Exn.interruptible_capture e ())) es;
+
 fun map_future f x =
   let
     val task = task_of x;
@@ -569,16 +583,12 @@
   in
     if extended then Future {promised = false, task = task, result = result}
     else
-      (singleton o forks)
+      (singleton o cond_forks)
         {name = "map_future", group = SOME group, deps = [task],
           pri = Task_Queue.pri_of_task task, interrupts = true}
         (fn () => f (join x))
   end;
 
-fun cond_forks args es =
-  if Multithreading.enabled () then forks args es
-  else map (fn e => value_result (Exn.interruptible_capture e ())) es;
-
 
 (* promised futures -- fulfilled by external means *)
 
diff -r 63cddfbc5a09 -r b7f9e764532a src/Pure/Concurrent/par_exn.ML
--- a/src/Pure/Concurrent/par_exn.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/Concurrent/par_exn.ML	Sun Aug 21 13:36:23 2011 +0200
@@ -43,7 +43,7 @@
   | par_exns exn = if Exn.is_interrupt exn then [] else [#2 (serial exn)];
 
 fun make exns =
-  (case Balanced_Tree.make (Ord_List.merge exn_ord) ([] :: map par_exns exns) of
+  (case Ord_List.unions exn_ord (map par_exns exns) of
     [] => Exn.Interrupt
   | es => Par_Exn es);
 
diff -r 63cddfbc5a09 -r b7f9e764532a src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/Concurrent/task_queue.ML	Sun Aug 21 13:36:23 2011 +0200
@@ -31,8 +31,8 @@
   val known_task: queue -> task -> bool
   val all_passive: queue -> bool
   val status: queue -> {ready: int, pending: int, running: int, passive: int}
-  val cancel: queue -> group -> task list
-  val cancel_all: queue -> group list
+  val cancel: queue -> group -> task list * Thread.thread list
+  val cancel_all: queue -> group list * Thread.thread list
   val finish: task -> queue -> bool * queue
   val enqueue_passive: group -> (unit -> bool) -> queue -> task * queue
   val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue
@@ -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);
@@ -248,12 +250,13 @@
   let
     val _ = cancel_group group Exn.Interrupt;
     val running =
-      Tasks.fold (fn (task, _) =>
-          (case get_job jobs task of Running thread => cons (task, thread) | _ => I))
-        (get_tasks groups (group_id group)) [];
-    val threads = fold (insert Thread.equal o #2) running [];
-    val _ = List.app Simple_Thread.interrupt_unsynchronized threads;
-  in map #1 running end;
+      Tasks.fold (fn (task, _) => fn (tasks, threads) =>
+          (case get_job jobs task of
+            Running thread => (task :: tasks, insert Thread.equal thread threads)
+          | Passive _ => (task :: tasks, threads)
+          | _ => (tasks, threads)))
+        (get_tasks groups (group_id group)) ([], []);
+  in running end;
 
 fun cancel_all (Queue {jobs, ...}) =
   let
@@ -266,9 +269,8 @@
           Running t => (insert eq_group group groups, insert Thread.equal t running)
         | _ => (groups, running))
       end;
-    val (running_groups, running) = Task_Graph.fold cancel_job jobs ([], []);
-    val _ = List.app Simple_Thread.interrupt_unsynchronized running;
-  in running_groups end;
+    val running = Task_Graph.fold cancel_job jobs ([], []);
+  in running end;
 
 
 (* finish *)
@@ -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 63cddfbc5a09 -r b7f9e764532a src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/General/graph.ML	Sun Aug 21 13:36:23 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 63cddfbc5a09 -r b7f9e764532a src/Pure/General/ord_list.ML
--- a/src/Pure/General/ord_list.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/General/ord_list.ML	Sun Aug 21 13:36:23 2011 +0200
@@ -14,6 +14,7 @@
   val remove: ('b * 'a -> order) -> 'b -> 'a T -> 'a T
   val subset: ('b * 'a -> order) -> 'b T * 'a T -> bool
   val union: ('a * 'a -> order) -> 'a T -> 'a T -> 'a T
+  val unions: ('a * 'a -> order) -> 'a T list -> 'a T
   val merge: ('a * 'a -> order) -> 'a T * 'a T -> 'a T
   val inter: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
   val subtract: ('b * 'a -> order) -> 'b T -> 'a T -> 'a T
@@ -86,6 +87,15 @@
           | GREATER => y :: unio lst1 ys);
   in if pointer_eq (list1, list2) then list1 else handle_same (unio list1) list2 end;
 
+fun unions ord lists =
+  let
+    fun unios (xs :: ys :: rest) acc = unios rest (union ord xs ys :: acc)
+      | unios [xs] (ys :: acc) = unios (union ord xs ys :: acc) []
+      | unios [xs] [] = xs
+      | unios [] [] = []
+      | unios [] acc = unios acc [];
+  in unios lists [] end;
+
 fun merge ord (list1, list2) = union ord list2 list1;
 
 (*intersection: filter second list for elements present in first list*)
diff -r 63cddfbc5a09 -r b7f9e764532a src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/General/table.ML	Sun Aug 21 13:36:23 2011 +0200
@@ -340,7 +340,7 @@
 in
 
 fun delete key tab = snd (snd (del (SOME key) tab));
-fun delete_safe key tab = delete key tab handle UNDEF _ => tab;
+fun delete_safe key tab = if defined tab key then delete key tab else tab;
 
 end;
 
diff -r 63cddfbc5a09 -r b7f9e764532a src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Aug 21 13:36:23 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 63cddfbc5a09 -r b7f9e764532a src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/PIDE/document.ML	Sun Aug 21 13:36:23 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);
@@ -371,7 +372,7 @@
                         |> set_result result;
                     in ((assigns, execs, [(name, node')]), node') end)
               end))
-      |> Future.join_results |> Par_Exn.release_all |> map #1;
+      |> Future.joins |> map #1;
 
     val state' = state
       |> fold (fold define_exec o #2) updates
diff -r 63cddfbc5a09 -r b7f9e764532a src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/Thy/thm_deps.ML	Sun Aug 21 13:36:23 2011 +0200
@@ -40,7 +40,7 @@
                path = "",
                parents = parents};
           in cons entry end;
-    val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
+    val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) [];
   in Present.display_graph (sort_wrt #ID deps) end;
 
 
@@ -66,7 +66,8 @@
     val used =
       Proofterm.fold_body_thms
         (fn (a, _, _) => a <> "" ? Symtab.update (a, ()))
-        (map (Proofterm.strip_thm o Thm.proof_body_of o #1 o #2) new_thms) Symtab.empty;
+        (map Proofterm.strip_thm (Thm.proof_bodies_of (map (#1 o #2) new_thms)))
+        Symtab.empty;
 
     fun is_unused a = not (Symtab.defined used a);
 
diff -r 63cddfbc5a09 -r b7f9e764532a src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/Thy/thy_info.ML	Sun Aug 21 13:36:23 2011 +0200
@@ -113,10 +113,6 @@
 val is_finished = is_none o get_deps;
 val master_directory = master_dir o get_deps;
 
-fun get_parents name =
-  thy_graph Graph.imm_preds name handle Graph.UNDEF _ =>
-    error (loader_msg "nothing known about theory" [name]);
-
 
 (* access theory *)
 
@@ -130,6 +126,8 @@
     SOME theory => theory
   | _ => error (loader_msg "undefined theory entry for" [name]));
 
+val get_imports = Thy_Load.imports_of o get_theory;
+
 fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () =>
   (case get_deps name of
     NONE => []
@@ -242,7 +240,7 @@
 
 fun check_deps dir name =
   (case lookup_deps name of
-    SOME NONE => (true, NONE, get_parents name)
+    SOME NONE => (true, NONE, get_imports name)
   | NONE =>
       let val {master, text, imports, ...} = Thy_Load.check_thy dir name
       in (false, SOME (make_deps master imports, text), imports) end
diff -r 63cddfbc5a09 -r b7f9e764532a src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/axclass.ML	Sun Aug 21 13:36:23 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 63cddfbc5a09 -r b7f9e764532a src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/proofterm.ML	Sun Aug 21 13:36:23 2011 +0200
@@ -37,17 +37,17 @@
 
   type oracle = string * term
   type pthm = serial * (string * term * proof_body future)
-  val join_body: proof_body -> unit
   val proof_of: proof_body -> proof
   val join_proof: proof_body future -> proof
   val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
   val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
+  val join_bodies: proof_body list -> unit
   val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
 
   val oracle_ord: oracle * oracle -> order
   val thm_ord: pthm * pthm -> order
-  val merge_oracles: oracle Ord_List.T -> oracle Ord_List.T -> oracle Ord_List.T
-  val merge_thms: pthm Ord_List.T -> pthm Ord_List.T -> pthm Ord_List.T
+  val unions_oracles: oracle Ord_List.T list -> oracle Ord_List.T
+  val unions_thms: pthm Ord_List.T list -> pthm Ord_List.T
   val all_oracles_of: proof_body -> oracle Ord_List.T
   val approximate_proof_body: proof -> proof_body
 
@@ -171,13 +171,11 @@
 type oracle = string * term;
 type pthm = serial * (string * term * proof_body future);
 
-fun join_thm (pthm: pthm) = ignore (Future.join (#3 (#2 pthm)));
-fun join_thms thms = (Future.join_results (map (#3 o #2) thms); List.app join_thm thms);
-fun join_body (PBody {thms, ...}) = join_thms thms;
-
 fun proof_of (PBody {proof, ...}) = proof;
 val join_proof = Future.join #> proof_of;
 
+fun join_thms (thms: pthm list) = ignore (Future.joins (map (#3 o #2) thms));
+
 
 (***** proof atoms *****)
 
@@ -208,6 +206,8 @@
           in (f (name, prop, body') x', seen') end);
   in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
 
+fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
+
 fun status_of bodies =
   let
     fun status (PBody {oracles, thms, ...}) x =
@@ -237,8 +237,8 @@
 val oracle_ord = prod_ord fast_string_ord Term_Ord.fast_term_ord;
 fun thm_ord ((i, _): pthm, (j, _)) = int_ord (j, i);
 
-val merge_oracles = Ord_List.union oracle_ord;
-val merge_thms = Ord_List.union thm_ord;
+val unions_oracles = Ord_List.unions oracle_ord;
+val unions_thms = Ord_List.unions thm_ord;
 
 val all_oracles_of =
   let
@@ -249,8 +249,8 @@
           let
             val body' = Future.join body;
             val (x', seen') = collect body' (x, Inttab.update (i, ()) seen);
-          in (merge_oracles oracles x', seen') end);
-  in fn body => #1 (collect body ([], Inttab.empty)) end;
+          in (if null oracles then x' else oracles :: x', seen') end);
+  in fn body => unions_oracles (#1 (collect body ([], Inttab.empty))) end;
 
 fun approximate_proof_body prf =
   let
@@ -1385,8 +1385,11 @@
 fun fulfill_norm_proof thy ps body0 =
   let
     val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
-    val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
-    val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
+    val oracles =
+      unions_oracles
+        (fold (fn (_, PBody {oracles, ...}) => not (null oracles) ? cons oracles) ps [oracles0]);
+    val thms =
+      unions_thms (fold (fn (_, PBody {thms, ...}) => not (null thms) ? cons thms) ps [thms0]);
     val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
 
     fun fill (Promise (i, prop, Ts)) =
@@ -1396,12 +1399,9 @@
       | fill _ = NONE;
     val (rules, procs) = get_data thy;
     val proof = rewrite_prf fst (rules, K (K fill) :: procs) proof0;
-    val _ = join_thms thms;
   in PBody {oracles = oracles, thms = thms, proof = proof} end;
 
-fun fulfill_proof_future _ [] postproc body =
-      if not (Multithreading.enabled ()) then Future.value (postproc (Future.join body))
-      else Future.map postproc body
+fun fulfill_proof_future _ [] postproc body = Future.map postproc body
   | fulfill_proof_future thy promises postproc body =
       (singleton o Future.forks)
         {name = "Proofterm.fulfill_proof_future", group = NONE,
@@ -1460,11 +1460,10 @@
     fun make_body0 proof0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
     val body0 =
       if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
-      else if not (Multithreading.enabled ()) then Future.value (make_body0 (full_proof0 ()))
       else
-        (singleton o Future.forks)
+        (singleton o Future.cond_forks)
           {name = "Proofterm.prepare_thm_proof", group = NONE,
-            deps = [], pri = ~1, interrupts = true}
+            deps = [], pri = 0, interrupts = true}
           (make_body0 o full_proof0);
 
     fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
diff -r 63cddfbc5a09 -r b7f9e764532a src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/sorts.ML	Sun Aug 21 13:36:23 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 63cddfbc5a09 -r b7f9e764532a src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Pure/thm.ML	Sun Aug 21 13:36:23 2011 +0200
@@ -95,9 +95,10 @@
   val weaken: cterm -> thm -> thm
   val weaken_sorts: sort list -> cterm -> cterm
   val extra_shyps: thm -> sort list
-  val join_proofs: thm list -> unit
+  val proof_bodies_of: thm list -> proof_body list
   val proof_body_of: thm -> proof_body
   val proof_of: thm -> proof
+  val join_proofs: thm list -> unit
   val status_of: thm -> {oracle: bool, unfinished: bool, failed: bool}
   val future: thm future -> cterm -> thm
   val derivation_name: thm -> string
@@ -491,8 +492,8 @@
     (Deriv {promises = ps2, body = PBody {oracles = oras2, thms = thms2, proof = prf2}}) =
   let
     val ps = Ord_List.union promise_ord ps1 ps2;
-    val oras = Proofterm.merge_oracles oras1 oras2;
-    val thms = Proofterm.merge_thms thms1 thms2;
+    val oras = Proofterm.unions_oracles [oras1, oras2];
+    val thms = Proofterm.unions_thms [thms1, thms2];
     val prf =
       (case ! Proofterm.proofs of
         2 => f prf1 prf2
@@ -510,18 +511,30 @@
 
 (* fulfilled proofs *)
 
-fun raw_body (Thm (Deriv {body, ...}, _)) = body;
+fun raw_body_of (Thm (Deriv {body, ...}, _)) = body;
+fun raw_promises_of (Thm (Deriv {promises, ...}, _)) = promises;
+
+fun join_promises [] = ()
+  | join_promises promises = join_promises_of (Future.joins (map snd promises))
+and join_promises_of thms = join_promises (maps raw_promises_of thms);
 
 fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
-  Proofterm.fulfill_norm_proof (Theory.deref thy_ref)
-    (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
-and fulfill_bodies futures = map fulfill_body (Par_Exn.release_all (Future.join_results futures));
+  Proofterm.fulfill_norm_proof (Theory.deref thy_ref) (fulfill_promises promises) body
+and fulfill_promises promises =
+  map fst promises ~~ map fulfill_body (Future.joins (map snd promises));
 
-fun join_proofs thms = ignore (map fulfill_body thms);
+fun proof_bodies_of thms =
+  let
+    val _ = join_promises_of thms;
+    val bodies = map fulfill_body thms;
+    val _ = Proofterm.join_bodies bodies;
+  in bodies end;
 
-fun proof_body_of thm = (Proofterm.join_body (raw_body thm); fulfill_body thm);
+val proof_body_of = singleton proof_bodies_of;
 val proof_of = Proofterm.proof_of o proof_body_of;
 
+val join_proofs = ignore o proof_bodies_of;
+
 
 (* derivation status *)
 
@@ -529,7 +542,7 @@
   let
     val ps = map (Future.peek o snd) promises;
     val bodies = body ::
-      map_filter (fn SOME (Exn.Res th) => SOME (raw_body th) | _ => NONE) ps;
+      map_filter (fn SOME (Exn.Res th) => SOME (raw_body_of th) | _ => NONE) ps;
     val {oracle, unfinished, failed} = Proofterm.status_of bodies;
   in
    {oracle = oracle,
@@ -552,7 +565,7 @@
     val _ = null hyps orelse err "bad hyps";
     val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
     val _ = forall (fn (j, _) => i <> j) promises orelse err "bad dependencies";
-    val _ = fulfill_bodies (map #2 promises);
+    val _ = join_promises promises;
   in thm end;
 
 fun future future_thm ct =
diff -r 63cddfbc5a09 -r b7f9e764532a src/Tools/Code/code_namespace.ML
--- a/src/Tools/Code/code_namespace.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Tools/Code/code_namespace.ML	Sun Aug 21 13:36:23 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 63cddfbc5a09 -r b7f9e764532a src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Tools/Code/code_preproc.ML	Sun Aug 21 13:36:23 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 63cddfbc5a09 -r b7f9e764532a src/Tools/Code/code_scala.ML
--- a/src/Tools/Code/code_scala.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Tools/Code/code_scala.ML	Sun Aug 21 13:36:23 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 63cddfbc5a09 -r b7f9e764532a src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Tools/Code/code_thingol.ML	Sun Aug 21 13:36:23 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 63cddfbc5a09 -r b7f9e764532a src/Tools/codegen.ML
--- a/src/Tools/codegen.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Tools/codegen.ML	Sun Aug 21 13:36:23 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 63cddfbc5a09 -r b7f9e764532a src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sun Aug 21 13:36:23 2011 +0200
@@ -54,19 +54,13 @@
   session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
   session_phase.tooltip = "Prover status"
 
-  private val interrupt = new Button("Interrupt") {
-    reactions += { case ButtonClicked(_) => Isabelle.session.interrupt }
-  }
-  interrupt.tooltip = "Broadcast interrupt to all prover tasks"
-
   private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
   logic.listenTo(logic.selection)
   logic.reactions += {
     case SelectionChanged(_) => Isabelle.Property("logic") = logic.selection.item.name
   }
 
-  private val controls =
-    new FlowPanel(FlowPanel.Alignment.Right)(session_phase, interrupt, logic)
+  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(session_phase, logic)
   add(controls.peer, BorderLayout.NORTH)
 
 
diff -r 63cddfbc5a09 -r b7f9e764532a src/Tools/nbe.ML
--- a/src/Tools/nbe.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Tools/nbe.ML	Sun Aug 21 13:36:23 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 63cddfbc5a09 -r b7f9e764532a src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Sat Aug 20 15:19:35 2011 -0700
+++ b/src/Tools/subtyping.ML	Sun Aug 21 13:36:23 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) =