diff --git a/src/Pure/Concurrent/task_queue.ML b/src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML
+++ b/src/Pure/Concurrent/task_queue.ML
@@ -1,436 +1,436 @@
 (*  Title:      Pure/Concurrent/task_queue.ML
     Author:     Makarius
 
 Ordered queue of grouped tasks.
 *)
 
 signature TASK_QUEUE =
 sig
   type group
   val new_group: group option -> group
   val group_id: group -> int
   val eq_group: group * group -> bool
   val cancel_group: group -> exn -> unit
   val is_canceled: group -> bool
   val group_status: group -> exn list
   val str_of_group: group -> string
   val str_of_groups: group -> string
   val urgent_pri: int
   type task
   val dummy_task: task
   val group_of_task: task -> group
   val name_of_task: task -> string
   val pri_of_task: task -> int
   val eq_task: task * task -> bool
   val str_of_task: task -> string
   val str_of_task_groups: task -> string
   val task_statistics: task -> Properties.T
   val running: task -> (unit -> 'a) -> 'a
   val joining: task -> (unit -> 'a) -> 'a
   val waiting: task -> task list -> (unit -> 'a) -> 'a
   type queue
   val empty: queue
   val group_tasks: queue -> group list -> task list
   val known_task: queue -> task -> bool
   val all_passive: queue -> bool
   val total_jobs: queue -> int
   val status: queue -> {ready: int, pending: int, running: int, passive: int, urgent: int}
   val cancel: queue -> group -> Thread.thread list
   val cancel_all: queue -> group list * Thread.thread list
   val finish: task -> queue -> bool * queue
   val enroll: Thread.thread -> string -> group -> queue -> task * queue
   val enqueue_passive: group -> string -> (unit -> bool) -> queue -> task * queue
   val enqueue: string -> group -> task list -> int -> (bool -> bool) -> queue -> task * queue
   val extend: task -> (bool -> bool) -> queue -> queue option
   val dequeue_passive: Thread.thread -> task -> queue -> bool option * queue
   val dequeue: Thread.thread -> bool -> queue -> (task * (bool -> bool) list) option * queue
   val dequeue_deps: Thread.thread -> task list -> queue ->
     (((task * (bool -> bool) list) option * task list) * queue)
 end;
 
 structure Task_Queue: TASK_QUEUE =
 struct
 
 val new_id = Counter.make ();
 
 
 (** nested groups of tasks **)
 
 (* groups *)
 
 abstype group = Group of
  {parent: group option,
   id: int,
   status: exn option Unsynchronized.ref}
 with
 
 fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status};
 
 fun new_group parent =
   make_group (parent, new_id (), Unsynchronized.ref NONE);
 
 fun group_id (Group {id, ...}) = id;
 fun eq_group (group1, group2) = group_id group1 = group_id group2;
 
 fun fold_groups f (g as Group {parent = NONE, ...}) a = f g a
   | fold_groups f (g as Group {parent = SOME group, ...}) a = fold_groups f group (f g a);
 
 
 (* group status *)
 
 local
 
 fun is_canceled_unsynchronized (Group {parent, status, ...}) =
   is_some (! status) orelse
     (case parent of NONE => false | SOME group => is_canceled_unsynchronized group);
 
 fun group_status_unsynchronized (Group {parent, status, ...}) =
   the_list (! status) @
     (case parent of NONE => [] | SOME group => group_status_unsynchronized group);
 
 val lock = Mutex.mutex ();
 fun SYNCHRONIZED e = Multithreading.synchronized "group_status" lock e;
 
 in
 
 fun cancel_group (Group {status, ...}) exn =
   SYNCHRONIZED (fn () =>
     Unsynchronized.change status (fn exns => SOME (Par_Exn.make (exn :: the_list exns))));
 
 fun is_canceled group =
   SYNCHRONIZED (fn () => is_canceled_unsynchronized group);
 
 fun group_status group =
   SYNCHRONIZED (fn () => group_status_unsynchronized group);
 
 end;
 
 fun str_of_group group =
   (is_canceled group ? enclose "(" ")") (string_of_int (group_id group));
 
 fun str_of_groups group =
   space_implode "/" (map str_of_group (rev (fold_groups cons group [])));
 
 end;
 
 
 (* tasks *)
 
 val urgent_pri = 1000;
 
 type timing = Time.time * Time.time * string list;  (*run, wait, wait dependencies*)
 
 val timing_start = (Time.zeroTime, Time.zeroTime, []): timing;
 
 fun new_timing () =
   if ! Multithreading.trace < 2 then NONE
   else SOME (Synchronized.var "timing" timing_start);
 
 abstype task = Task of
  {group: group,
   name: string,
   id: int,
   pri: int option,
   timing: timing Synchronized.var option,
   pos: Position.T}
 with
 
 val dummy_task =
   Task {group = new_group NONE, name = "", id = 0, pri = NONE, timing = NONE,
     pos = Position.none};
 
 fun new_task group name pri =
   Task {group = group, name = name, id = new_id (), pri = pri, timing = new_timing (),
     pos = Position.thread_data ()};
 
 fun group_of_task (Task {group, ...}) = group;
 fun name_of_task (Task {name, ...}) = name;
 fun id_of_task (Task {id, ...}) = id;
 fun pri_of_task (Task {pri, ...}) = the_default 0 pri;
 
 fun eq_task (task1, task2) = id_of_task task1 = id_of_task task2;
 
 fun str_of_task (Task {name, id, ...}) =
   if name = "" then string_of_int id else string_of_int id ^ " (" ^ name ^ ")";
 
 fun str_of_task_groups task = str_of_task task ^ " in " ^ str_of_groups (group_of_task task);
 
 fun update_timing update (Task {timing, ...}) e =
   Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
     let
       val start = Time.now ();
       val result = Exn.capture (restore_attributes e) ();
       val t = Time.now () - start;
       val _ = (case timing of NONE => () | SOME var => Synchronized.change var (update t));
     in Exn.release result end) ();
 
 fun task_ord (Task {id = id1, pri = pri1, ...}, Task {id = id2, pri = pri2, ...}) =
   prod_ord (rev_order o option_ord int_ord) int_ord ((pri1, id1), (pri2, id2));
 
 fun task_statistics (Task {name, id, timing, pos, ...}) =
   let
     val (run, wait, wait_deps) =
       (case timing of NONE => timing_start | SOME var => Synchronized.value var);
     fun micros time = string_of_int (Time.toNanoseconds time div 1000);
   in
     [("now", Value.print_real (Time.toReal (Time.now ()))),
      ("task_name", name), ("task_id", Value.print_int id),
      ("run", micros run), ("wait", micros wait), ("wait_deps", commas wait_deps)] @
     Position.properties_of pos
   end;
 
 end;
 
 structure Tasks = Set(type key = task val ord = task_ord);
-structure Task_Graph = Graph(type key = task val ord = task_ord);
+structure Task_Graph = Graph(Tasks.Key);
 
 
 (* timing *)
 
 fun running task =
   update_timing (fn t => fn (a, b, ds) => (a + t, b, ds)) task;
 
 fun joining task =
   update_timing (fn t => fn (a, b, ds) => (a - t, b, ds)) task;
 
 fun waiting task deps =
   update_timing (fn t => fn (a, b, ds) =>
     (a - t, b + t,
       if ! Multithreading.trace > 0
       then fold (insert (op =) o name_of_task) deps ds else ds)) task;
 
 
 
 (** queue of jobs and groups **)
 
 (* known group members *)
 
 type groups = Tasks.T Inttab.table;
 
 fun get_tasks (groups: groups) gid =
   the_default Tasks.empty (Inttab.lookup groups gid);
 
 fun add_task (gid, task) groups =
   Inttab.update (gid, Tasks.insert task (get_tasks groups gid)) groups;
 
 fun del_task (gid, task) groups =
   let val tasks = Tasks.remove task (get_tasks groups gid) in
     if Tasks.is_empty tasks then Inttab.delete_safe gid groups
     else Inttab.update (gid, tasks) groups
   end;
 
 
 (* job dependency graph *)
 
 datatype job =
   Job of (bool -> bool) list |
   Running of Thread.thread |
   Passive of unit -> bool;
 
 type jobs = job Task_Graph.T;
 
 fun get_job (jobs: jobs) task = Task_Graph.get_node jobs task;
 fun set_job task job (jobs: jobs) = Task_Graph.map_node task (K job) jobs;
 
 fun add_job task dep (jobs: jobs) =
   Task_Graph.add_edge (dep, task) jobs handle Task_Graph.UNDEF _ => jobs;
 
 
 (* queue *)
 
 datatype queue = Queue of {groups: groups, jobs: jobs, urgent: int, total: int};
 
 fun make_queue groups jobs urgent total =
   Queue {groups = groups, jobs = jobs, urgent = urgent, total = total};
 
 val empty = make_queue Inttab.empty Task_Graph.empty 0 0;
 
 fun group_tasks (Queue {groups, ...}) gs =
   fold (fn g => fn tasks => Tasks.merge (tasks, get_tasks groups (group_id g)))
     gs Tasks.empty
   |> Tasks.dest;
 
 fun known_task (Queue {jobs, ...}) task = can (Task_Graph.get_entry jobs) task;
 
 
 (* job status *)
 
 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;
 
 fun ready_job_urgent false = ready_job
   | ready_job_urgent true = (fn entry as (task, _) =>
       if pri_of_task task >= urgent_pri then ready_job entry else NONE);
 
 fun active_job (task, (Running _, _)) = SOME (task, [])
   | active_job arg = ready_job arg;
 
 fun all_passive (Queue {jobs, ...}) = is_none (Task_Graph.get_first active_job jobs);
 
 fun total_jobs (Queue {total, ...}) = total;
 
 
 (* queue status *)
 
 fun status (Queue {jobs, urgent, ...}) =
   let
     val (x, y, z, w) =
       Task_Graph.fold (fn (_, (job, (deps, _))) => fn (x, y, z, w) =>
           (case job of
             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);
   in {ready = x, pending = y, running = z, passive = w, urgent = urgent} end;
 
 
 
 (** task queue operations **)
 
 (* cancel -- peers and sub-groups *)
 
 fun cancel (Queue {groups, jobs, ...}) group =
   let
     val _ = cancel_group group Exn.Interrupt;
     val running =
       Tasks.fold (fn task =>
           (case get_job jobs task of Running thread => insert Thread.equal thread | _ => I))
         (get_tasks groups (group_id group)) [];
   in running end;
 
 fun cancel_all (Queue {jobs, ...}) =
   let
     fun cancel_job (task, (job, _)) (groups, running) =
       let
         val group = group_of_task task;
         val _ = cancel_group group Exn.Interrupt;
       in
         (case job of
           Running t => (insert eq_group group groups, insert Thread.equal t running)
         | _ => (groups, running))
       end;
     val running = Task_Graph.fold cancel_job jobs ([], []);
   in running end;
 
 
 (* finish *)
 
 fun finish task (Queue {groups, jobs, urgent, total}) =
   let
     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 total' = total - 1;
     val maximal = Task_Graph.is_maximal jobs task;
   in (maximal, make_queue groups' jobs' urgent total') end;
 
 
 (* enroll *)
 
 fun enroll thread name group (Queue {groups, jobs, urgent, total}) =
   let
     val task = new_task group name NONE;
     val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
     val jobs' = jobs |> Task_Graph.new_node (task, Running thread);
     val total' = total + 1;
   in (task, make_queue groups' jobs' urgent total') end;
 
 
 (* enqueue *)
 
 fun enqueue_passive group name abort (Queue {groups, jobs, urgent, total}) =
   let
     val task = new_task group name NONE;
     val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
     val jobs' = jobs |> Task_Graph.new_node (task, Passive abort);
     val total' = total + 1;
   in (task, make_queue groups' jobs' urgent total') end;
 
 fun enqueue name group deps pri job (Queue {groups, jobs, urgent, total}) =
   let
     val task = new_task group name (SOME pri);
     val groups' = fold_groups (fn g => add_task (group_id g, task)) group groups;
     val jobs' = jobs
       |> Task_Graph.new_node (task, Job [job])
       |> fold (add_job task) deps;
     val urgent' = if pri >= urgent_pri then urgent + 1 else urgent;
     val total' = total + 1;
   in (task, make_queue groups' jobs' urgent' total') end;
 
 fun extend task job (Queue {groups, jobs, urgent, total}) =
   (case try (get_job jobs) task of
     SOME (Job list) => SOME (make_queue groups (set_job task (Job (job :: list)) jobs) urgent total)
   | _ => NONE);
 
 
 (* dequeue *)
 
 fun dequeue_passive thread task (queue as Queue {groups, jobs, urgent, total}) =
   (case try (get_job jobs) task of
     SOME (Passive _) =>
       let val jobs' = set_job task (Running thread) jobs
       in (SOME true, make_queue groups jobs' urgent total) end
   | SOME _ => (SOME false, queue)
   | NONE => (NONE, queue));
 
 fun dequeue thread urgent_only (queue as Queue {groups, jobs, urgent, total}) =
   if not urgent_only orelse urgent > 0 then
     (case Task_Graph.get_first (ready_job_urgent urgent_only) jobs of
       SOME (result as (task, _)) =>
         let
           val jobs' = set_job task (Running thread) jobs;
           val urgent' = if pri_of_task task >= urgent_pri then urgent - 1 else urgent;
         in (SOME result, make_queue groups jobs' urgent' total) end
     | NONE => (NONE, queue))
   else (NONE, queue);
 
 
 (* dequeue wrt. dynamic dependencies *)
 
 fun dequeue_deps thread deps (queue as Queue {groups, jobs, urgent, total}) =
   let
     fun ready [] rest = (NONE, rev rest)
       | ready (task :: tasks) rest =
           (case try (Task_Graph.get_entry jobs) task of
             NONE => ready tasks rest
           | SOME (_, entry) =>
               (case ready_job (task, entry) of
                 NONE => ready tasks (task :: rest)
               | some => (some, fold cons rest tasks)));
 
     fun ready_dep _ [] = NONE
       | ready_dep seen (task :: tasks) =
           if Tasks.member seen task then ready_dep seen tasks
           else
             let val entry as (_, (ds, _)) = #2 (Task_Graph.get_entry jobs task) in
               (case ready_job (task, entry) of
                 NONE => ready_dep (Tasks.insert task seen) (Task_Graph.Keys.dest ds @ tasks)
               | some => some)
             end;
 
     fun result (res as (task, _)) deps' =
       let
         val jobs' = set_job task (Running thread) jobs;
         val urgent' = if pri_of_task task >= urgent_pri then urgent - 1 else urgent;
       in ((SOME res, deps'), make_queue groups jobs' urgent' total) end;
   in
     (case ready deps [] of
       (SOME res, deps') => result res deps'
     | (NONE, deps') =>
         (case ready_dep Tasks.empty deps' of
           SOME res => result res deps'
         | NONE => ((NONE, deps'), queue)))
   end;
 
 
 (* toplevel pretty printing *)
 
 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_task);
 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_group);
 
 end;
diff --git a/src/Pure/General/graph.ML b/src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML
+++ b/src/Pure/General/graph.ML
@@ -1,357 +1,360 @@
 (*  Title:      Pure/General/graph.ML
     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
 
 Directed graphs.
 *)
 
 signature GRAPH =
 sig
+  structure Key: KEY
   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
   exception UNDEF of key
   val empty: 'a T
   val is_empty: 'a T -> bool
   val keys: '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 get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T))        (*exception UNDEF*)
   val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
   val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
   val map: (key -> 'a -> 'b) -> 'a T -> 'b T
   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 strong_conn: 'a T -> key list list
   val map_strong_conn: ((key * 'a) list -> 'b list) -> 'a T -> 'b T
   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 is_isolated: 'a T -> key -> bool
   val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
   val default_node: key * 'a -> 'a T -> 'a T
   val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
   val is_edge: 'a T -> key * key -> bool
   val add_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
   val del_edge: key * key -> 'a T -> 'a T                             (*exception UNDEF*)
   val restrict: (key -> bool) -> 'a T -> 'a T
   val dest: 'a T -> ((key * 'a) * key list) list
   val make: ((key * 'a) * key list) list -> 'a T                      (*exception DUP | UNDEF*)
   val merge: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T                 (*exception DUP*)
   val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
     'a T * 'a T -> 'a T                                               (*exception DUP*)
   val irreducible_paths: 'a T -> key * key -> key list list
   exception CYCLES of key list list
   val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception UNDEF | CYCLES*)
   val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception UNDEF | CYCLES*)
   val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T         (*exception CYCLES*)
   val topological_order: 'a T -> key list
   val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception UNDEF | CYCLES*)
   val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
   exception DEP of key * key
   val schedule: ((key * 'b) list -> key * 'a -> 'b) -> 'a T -> 'b list  (*exception DEP*)
   val encode: key XML.Encode.T -> 'a XML.Encode.T -> 'a T XML.Encode.T
   val decode: key XML.Decode.T -> 'a XML.Decode.T -> 'a T XML.Decode.T
 end;
 
 functor Graph(Key: KEY): GRAPH =
 struct
 
 (* keys *)
 
+structure Key = Key;
 type key = Key.key;
+
 val eq_key = is_equal o Key.ord;
 
 structure Table = Table(Key);
 structure Set = Set(Key);
 
 structure Keys =
 struct
 
 abstype T = Keys of Set.T
 with
 
 val empty = Keys Set.empty;
 fun is_empty (Keys set) = Set.is_empty set;
 
 fun member (Keys set) = Set.member set;
 fun insert x (Keys set) = Keys (Set.insert x set);
 fun remove x (Keys set) = Keys (Set.remove x set);
 
 fun fold f (Keys set) = Set.fold f set;
 fun fold_rev f (Keys set) = Set.fold_rev f set;
 
 fun dest keys = fold_rev cons keys [];
 
 fun filter P keys = fold (fn x => P x ? insert x) keys empty;
 
 end;
 end;
 
 
 (* graphs *)
 
 datatype 'a T = Graph of ('a * (Keys.T * Keys.T)) Table.table;
 
 exception DUP = Table.DUP;
 exception UNDEF = Table.UNDEF;
 exception SAME = Table.SAME;
 
 val empty = Graph Table.empty;
 fun is_empty (Graph tab) = Table.is_empty tab;
 fun keys (Graph tab) = Table.keys tab;
 
 fun get_first f (Graph tab) = Table.get_first f tab;
 fun fold_graph f (Graph tab) = Table.fold f tab;
 
 fun get_entry (Graph tab) x =
   (case Table.lookup_key tab x of
     SOME entry => entry
   | NONE => raise UNDEF x);
 
 fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (#2 (get_entry G x))) tab);
 
 
 (* nodes *)
 
 fun get_node G = #1 o #2 o get_entry G;
 
 fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));
 
 fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab);
 
 
 (* reachability *)
 
 (*nodes reachable from xs -- topologically sorted for acyclic graphs*)
 fun reachable next xs =
   let
     fun reach x (rs, R) =
       if Keys.member R x then (rs, R)
       else Keys.fold_rev 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 ([], 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);
 
 (*strongly connected components; see: David King and John Launchbury,
   "Structuring Depth First Search Algorithms in Haskell"*)
 fun strong_conn G =
   rev (filter_out null (#1 (reachable (imm_preds G) (all_succs G (keys G)))));
 
 fun map_strong_conn f G =
   let
     val xss = strong_conn G;
     fun map' xs =
       fold2 (curry Table.update) xs (f (AList.make (get_node G) xs));
     val tab' = Table.empty
       |> fold map' xss;
   in map_nodes (fn x => fn _ => the (Table.lookup tab' x)) G end;
 
 
 (* 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);
 
 fun is_isolated G x = is_minimal G x andalso is_maximal G x;
 
 
 (* node operations *)
 
 fun new_node (x, info) (Graph tab) =
   Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab);
 
 fun default_node (x, info) (Graph tab) =
   Graph (Table.default (x, (info, (Keys.empty, Keys.empty))) tab);
 
 fun del_node x (G as Graph tab) =
   let
     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
       |> Keys.fold (del_adjacent apsnd) preds
       |> Keys.fold (del_adjacent apfst) succs)
   end;
 
 fun restrict pred G =
   fold_graph (fn (x, _) => not (pred x) ? del_node x) G G;
 
 
 (* edge operations *)
 
 fun is_edge (Graph tab) (x, y) =
   (case Table.lookup tab x of
     SOME (_, (_, succs)) => Keys.member succs y
   | NONE => 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, (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, (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 =
   fold_graph (fn (x, (_, (_, succs))) =>
     Keys.fold (fn y => not (is_edge G2 (x, y)) ? cons (x, y)) succs) G1 [];
 
 fun edges G = diff_edges G empty;
 
 
 (* dest and make *)
 
 fun dest G = fold_graph (fn (x, (i, (_, succs))) => cons ((x, i), Keys.dest succs)) G [];
 
 fun make entries =
   empty
   |> fold (new_node o fst) entries
   |> fold (fn ((x, _), ys) => fold (fn y => add_edge (x, y)) ys) entries;
 
 
 (* join and merge *)
 
 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
     if pointer_eq (G1, G2) then G1
     else fold add_edge (edges G2) (Graph (Table.join join_node (tab1, Table.map (K no_edges) tab2)))
   end;
 
 fun gen_merge add eq (G1 as Graph tab1, G2 as Graph tab2) =
   let fun eq_node ((i1, _), (i2, _)) = eq (i1, i2) in
     if pointer_eq (G1, G2) then G1
     else fold add (edges G2) (Graph (Table.merge eq_node (tab1, Table.map (K no_edges) tab2)))
   end;
 
 fun merge eq GG = gen_merge add_edge eq GG;
 
 
 (* irreducible paths -- Hasse diagram *)
 
 fun irreducible_preds G X path z =
   let
     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 (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 (immediate_preds G z) [] end;
 
 fun irreducible_paths G (x, y) =
   let
     val (_, X) = reachable (imm_succs G) [x];
     fun paths path z =
       if eq_key (x, z) then cons (z :: path)
       else fold (paths (z :: path)) (irreducible_preds G X path z);
   in if eq_key (x, y) andalso not (is_edge G (x, x)) then [[]] else paths [] y [] end;
 
 
 (* maintain acyclic graphs *)
 
 exception CYCLES of key list list;
 
 fun add_edge_acyclic (x, y) G =
   if is_edge G (x, y) then G
   else
     (case irreducible_paths G (y, x) of
       [] => add_edge (x, y) G
     | cycles => raise CYCLES (map (cons x) cycles));
 
 fun add_deps_acyclic (y, xs) = fold (fn x => add_edge_acyclic (x, y)) xs;
 
 fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG;
 
 fun topological_order G = minimals G |> all_succs G;
 
 
 (* maintain transitive acyclic graphs *)
 
 fun add_edge_trans_acyclic (x, y) G =
   add_edge_acyclic (x, y) G
   |> fold_product (curry add_edge) (all_preds G [x]) (all_succs G [y]);
 
 fun merge_trans_acyclic eq (G1, G2) =
   if pointer_eq (G1, G2) then G1
   else
     merge_acyclic eq (G1, G2)
     |> fold add_edge_trans_acyclic (diff_edges G1 G2)
     |> fold add_edge_trans_acyclic (diff_edges G2 G1);
 
 
 (* schedule acyclic graph *)
 
 exception DEP of key * key;
 
 fun schedule f G =
   let
     val xs = topological_order G;
     val results = (xs, Table.empty) |-> fold (fn x => fn tab =>
       let
         val a = get_node G x;
         val deps = immediate_preds G x |> map (fn y =>
           (case Table.lookup tab y of
             SOME b => (y, b)
           | NONE => raise DEP (x, y)));
       in Table.update (x, f deps (x, a)) tab end);
   in map (the o Table.lookup results) xs end;
 
 
 (* XML data representation *)
 
 fun encode key info G =
   dest G |>
     let open XML.Encode
     in list (pair (pair key info) (list key)) end;
 
 fun decode key info body =
   body |>
     let open XML.Decode
     in list (pair (pair key info) (list key)) end |> make;
 
 
 (*final declarations of this structure!*)
 val map = map_nodes;
 val fold = fold_graph;
 
 end;
 
-structure Graph = Graph(type key = string val ord = fast_string_ord);
+structure Graph = Graph(Symtab.Key);
 structure String_Graph = Graph(type key = string val ord = string_ord);
-structure Int_Graph = Graph(type key = int val ord = int_ord);
+structure Int_Graph = Graph(Inttab.Key);
diff --git a/src/Pure/General/set.ML b/src/Pure/General/set.ML
--- a/src/Pure/General/set.ML
+++ b/src/Pure/General/set.ML
@@ -1,343 +1,346 @@
 (*  Title:      Pure/General/set.ML
     Author:     Makarius
 
 Efficient representation of sets (see also Pure/General/table.ML).
 *)
 
 signature SET =
 sig
+  structure Key: KEY
   type elem
   type T
   val size: T -> int
   val empty: T
   val build: (T -> T) -> T
   val is_empty: T -> bool
   val is_single: T -> bool
   val fold: (elem -> 'a -> 'a) -> T -> 'a -> 'a
   val fold_rev: (elem -> 'a -> 'a) -> T -> 'a -> 'a
   val dest: T -> elem list
   val exists: (elem -> bool) -> T -> bool
   val forall: (elem -> bool) -> T -> bool
   val get_first: (elem -> 'a option) -> T -> 'a option
   val member: T -> elem -> bool
   val subset: T * T -> bool
   val ord: T ord
   val insert: elem -> T -> T
   val make: elem list -> T
   val merge: T * T -> T
   val remove: elem -> T -> T
   val subtract: T -> T -> T
 end;
 
 functor Set(Key: KEY): SET =
 struct
 
+structure Key = Key;
+type elem = Key.key;
+
+
 (* datatype *)
 
-type elem = Key.key;
-
 datatype T =
   Empty |
   Branch2 of T * elem * T |
   Branch3 of T * elem * T * elem * T;
 
 
 (* size *)
 
 local
   fun add_size Empty n = n
     | add_size (Branch2 (left, _, right)) n =
         n + 1 |> add_size left |> add_size right
     | add_size (Branch3 (left, _, mid, _, right)) n =
         n + 2 |> add_size left |> add_size mid |> add_size right;
 in
   fun size set = add_size set 0;
 end;
 
 
 (* empty and single *)
 
 val empty = Empty;
 
 fun build (f: T -> T) = f empty;
 
 fun is_empty Empty = true
   | is_empty _ = false;
 
 fun is_single (Branch2 (Empty, _, Empty)) = true
   | is_single _ = false;
 
 
 (* fold combinators *)
 
 fun fold_set f =
   let
     fun fold Empty x = x
       | fold (Branch2 (left, e, right)) x =
           fold right (f e (fold left x))
       | fold (Branch3 (left, e1, mid, e2, right)) x =
           fold right (f e2 (fold mid (f e1 (fold left x))));
   in fold end;
 
 fun fold_rev_set f =
   let
     fun fold Empty x = x
       | fold (Branch2 (left, e, right)) x =
           fold left (f e (fold right x))
       | fold (Branch3 (left, e1, mid, e2, right)) x =
           fold left (f e1 (fold mid (f e2 (fold right x))));
   in fold end;
 
 fun dest tab = fold_rev_set cons tab [];
 
 
 (* exists and forall *)
 
 fun exists pred =
   let
     fun ex Empty = false
       | ex (Branch2 (left, e, right)) =
           ex left orelse pred e orelse ex right
       | ex (Branch3 (left, e1, mid, e2, right)) =
           ex left orelse pred e1 orelse ex mid orelse pred e2 orelse ex right;
   in ex end;
 
 fun forall pred = not o exists (not o pred);
 
 
 (* get_first *)
 
 fun get_first f =
   let
     fun get Empty = NONE
       | get (Branch2 (left, e, right)) =
           (case get left of
             NONE =>
               (case f e of
                 NONE => get right
               | some => some)
           | some => some)
       | get (Branch3 (left, e1, mid, e2, right)) =
           (case get left of
             NONE =>
               (case f e1 of
                 NONE =>
                   (case get mid of
                     NONE =>
                       (case f e2 of
                         NONE => get right
                       | some => some)
                   | some => some)
               | some => some)
           | some => some);
   in get end;
 
 
 (* member *)
 
 fun member set elem =
   let
     fun mem Empty = false
       | mem (Branch2 (left, e, right)) =
           (case Key.ord (elem, e) of
             LESS => mem left
           | EQUAL => true
           | GREATER => mem right)
       | mem (Branch3 (left, e1, mid, e2, right)) =
           (case Key.ord (elem, e1) of
             LESS => mem left
           | EQUAL => true
           | GREATER =>
               (case Key.ord (elem, e2) of
                 LESS => mem mid
               | EQUAL => true
               | GREATER => mem right));
   in mem set end;
 
 
 (* subset and order *)
 
 fun subset (set1, set2) = forall (member set2) set1;
 
 val ord =
   pointer_eq_ord (fn sets =>
     (case int_ord (apply2 size sets) of
       EQUAL =>
         if subset sets then EQUAL
         else dict_ord Key.ord (apply2 dest sets)
     | ord => ord));
 
 
 (* insert *)
 
 datatype growth = Stay of T | Sprout of T * elem * T;
 
 fun insert elem set =
   if member set elem then set
   else
     let
       fun ins Empty = Sprout (Empty, elem, Empty)
         | ins (Branch2 (left, e, right)) =
             (case Key.ord (elem, e) of
               LESS =>
                 (case ins left of
                   Stay left' => Stay (Branch2 (left', e, right))
                 | Sprout (left1, e', left2) => Stay (Branch3 (left1, e', left2, e, right)))
             | EQUAL => Stay (Branch2 (left, e, right))
             | GREATER =>
                 (case ins right of
                   Stay right' => Stay (Branch2 (left, e, right'))
                 | Sprout (right1, e', right2) =>
                     Stay (Branch3 (left, e, right1, e', right2))))
         | ins (Branch3 (left, e1, mid, e2, right)) =
             (case Key.ord (elem, e1) of
               LESS =>
                 (case ins left of
                   Stay left' => Stay (Branch3 (left', e1, mid, e2, right))
                 | Sprout (left1, e', left2) =>
                     Sprout (Branch2 (left1, e', left2), e1, Branch2 (mid, e2, right)))
             | EQUAL => Stay (Branch3 (left, e1, mid, e2, right))
             | GREATER =>
                 (case Key.ord (elem, e2) of
                   LESS =>
                     (case ins mid of
                       Stay mid' => Stay (Branch3 (left, e1, mid', e2, right))
                     | Sprout (mid1, e', mid2) =>
                         Sprout (Branch2 (left, e1, mid1), e', Branch2 (mid2, e2, right)))
                 | EQUAL => Stay (Branch3 (left, e1, mid, e2, right))
                 | GREATER =>
                     (case ins right of
                       Stay right' => Stay (Branch3 (left, e1, mid, e2, right'))
                     | Sprout (right1, e', right2) =>
                         Sprout (Branch2 (left, e1, mid), e2, Branch2 (right1, e', right2)))));
     in
       (case ins set of
         Stay set' => set'
       | Sprout br => Branch2 br)
     end;
 
 fun make elems = build (fold insert elems);
 
 fun merge (set1, set2) =
   if pointer_eq (set1, set2) then set1
   else if is_empty set1 then set2
   else if is_empty set2 then set1
   else if size set1 >= size set2
   then fold_set insert set2 set1
   else fold_set insert set1 set2;
 
 
 (* remove *)
 
 local
 
 fun compare NONE _ = LESS
   | compare (SOME e1) e2 = Key.ord (e1, e2);
 
 fun if_eq EQUAL x y = x
   | if_eq _ x y = y;
 
 exception UNDEF of elem;
 
 (*literal copy from table.ML -- by Stefan Berghofer*)
 fun del (SOME k) Empty = raise UNDEF k
   | del NONE (Branch2 (Empty, p, Empty)) = (p, (true, Empty))
   | del NONE (Branch3 (Empty, p, Empty, q, Empty)) =
       (p, (false, Branch2 (Empty, q, Empty)))
   | del k (Branch2 (Empty, p, Empty)) =
       (case compare k p of
         EQUAL => (p, (true, Empty))
       | _ => raise UNDEF (the k))
   | del k (Branch3 (Empty, p, Empty, q, Empty)) =
       (case compare k p of
         EQUAL => (p, (false, Branch2 (Empty, q, Empty)))
       | _ =>
         (case compare k q of
           EQUAL => (q, (false, Branch2 (Empty, p, Empty)))
         | _ => raise UNDEF (the k)))
   | del k (Branch2 (l, p, r)) =
       (case compare k p of
         LESS =>
           (case del k l of
             (p', (false, l')) => (p', (false, Branch2 (l', p, r)))
           | (p', (true, l')) => (p', case r of
               Branch2 (rl, rp, rr) =>
                 (true, Branch3 (l', p, rl, rp, rr))
             | Branch3 (rl, rp, rm, rq, rr) => (false, Branch2
                 (Branch2 (l', p, rl), rp, Branch2 (rm, rq, rr)))))
       | ord =>
           (case del (if_eq ord NONE k) r of
             (p', (false, r')) => (p', (false, Branch2 (l, if_eq ord p' p, r')))
           | (p', (true, r')) => (p', case l of
               Branch2 (ll, lp, lr) =>
                 (true, Branch3 (ll, lp, lr, if_eq ord p' p, r'))
             | Branch3 (ll, lp, lm, lq, lr) => (false, Branch2
                 (Branch2 (ll, lp, lm), lq, Branch2 (lr, if_eq ord p' p, r'))))))
   | del k (Branch3 (l, p, m, q, r)) =
       (case compare k q of
         LESS =>
           (case compare k p of
             LESS =>
               (case del k l of
                 (p', (false, l')) => (p', (false, Branch3 (l', p, m, q, r)))
               | (p', (true, l')) => (p', (false, case (m, r) of
                   (Branch2 (ml, mp, mr), Branch2 _) =>
                     Branch2 (Branch3 (l', p, ml, mp, mr), q, r)
                 | (Branch3 (ml, mp, mm, mq, mr), _) =>
                     Branch3 (Branch2 (l', p, ml), mp, Branch2 (mm, mq, mr), q, r)
                 | (Branch2 (ml, mp, mr), Branch3 (rl, rp, rm, rq, rr)) =>
                     Branch3 (Branch2 (l', p, ml), mp, Branch2 (mr, q, rl), rp,
                       Branch2 (rm, rq, rr)))))
           | ord =>
               (case del (if_eq ord NONE k) m of
                 (p', (false, m')) =>
                   (p', (false, Branch3 (l, if_eq ord p' p, m', q, r)))
               | (p', (true, m')) => (p', (false, case (l, r) of
                   (Branch2 (ll, lp, lr), Branch2 _) =>
                     Branch2 (Branch3 (ll, lp, lr, if_eq ord p' p, m'), q, r)
                 | (Branch3 (ll, lp, lm, lq, lr), _) =>
                     Branch3 (Branch2 (ll, lp, lm), lq,
                       Branch2 (lr, if_eq ord p' p, m'), q, r)
                 | (_, Branch3 (rl, rp, rm, rq, rr)) =>
                     Branch3 (l, if_eq ord p' p, Branch2 (m', q, rl), rp,
                       Branch2 (rm, rq, rr))))))
       | ord =>
           (case del (if_eq ord NONE k) r of
             (q', (false, r')) =>
               (q', (false, Branch3 (l, p, m, if_eq ord q' q, r')))
           | (q', (true, r')) => (q', (false, case (l, m) of
               (Branch2 _, Branch2 (ml, mp, mr)) =>
                 Branch2 (l, p, Branch3 (ml, mp, mr, if_eq ord q' q, r'))
             | (_, Branch3 (ml, mp, mm, mq, mr)) =>
                 Branch3 (l, p, Branch2 (ml, mp, mm), mq,
                   Branch2 (mr, if_eq ord q' q, r'))
             | (Branch3 (ll, lp, lm, lq, lr), Branch2 (ml, mp, mr)) =>
                 Branch3 (Branch2 (ll, lp, lm), lq, Branch2 (lr, p, ml), mp,
                   Branch2 (mr, if_eq ord q' q, r'))))));
 
 in
 
 fun remove elem set =
   if member set elem then snd (snd (del (SOME elem) set)) else set;
 
 val subtract = fold_set remove;
 
 end;
 
 
 (* ML pretty-printing *)
 
 val _ =
   ML_system_pp (fn depth => fn _ => fn set =>
     ML_Pretty.to_polyml
       (ML_Pretty.enum "," "{" "}" (ML_Pretty.from_polyml o ML_system_pretty) (dest set, depth)));
 
 
 (*final declarations of this structure!*)
 val fold = fold_set;
 val fold_rev = fold_rev_set;
 
 end;
 
-structure Intset = Set(type key = int val ord = int_ord);
-structure Symset = Set(type key = string val ord = fast_string_ord);
+structure Intset = Set(Inttab.Key);
+structure Symset = Set(Symtab.Key);
diff --git a/src/Pure/General/table.ML b/src/Pure/General/table.ML
--- a/src/Pure/General/table.ML
+++ b/src/Pure/General/table.ML
@@ -1,484 +1,486 @@
 (*  Title:      Pure/General/table.ML
     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
 
 Generic tables.  Efficient purely functional implementation using
 balanced 2-3 trees.
 *)
 
 signature KEY =
 sig
   type key
   val ord: key ord
 end;
 
 signature TABLE =
 sig
+  structure Key: KEY
   type key
   type 'a table
   exception DUP of key
   exception SAME
   exception UNDEF of key
   val empty: 'a table
   val build: ('a table -> 'a table) -> 'a table
   val is_empty: 'a table -> bool
   val is_single: 'a table -> bool
   val map: (key -> 'a -> 'b) -> 'a table -> 'b table
   val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
   val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
   val dest: 'a table -> (key * 'a) list
   val keys: 'a table -> key list
   val min: 'a table -> (key * 'a) option
   val max: 'a table -> (key * 'a) option
   val exists: (key * 'a -> bool) -> 'a table -> bool
   val forall: (key * 'a -> bool) -> 'a table -> bool
   val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
   val lookup_key: 'a table -> key -> (key * 'a) option
   val lookup: 'a table -> key -> 'a option
   val defined: 'a table -> key -> bool
   val update: key * 'a -> 'a table -> 'a table
   val update_new: key * 'a -> 'a table -> 'a table                     (*exception DUP*)
   val default: key * 'a -> 'a table -> 'a table
   val map_entry: key -> ('a -> 'a) (*exception SAME*) -> 'a table -> 'a table
   val map_default: key * 'a -> ('a -> 'a) -> 'a table -> 'a table
   val make: (key * 'a) list -> 'a table                                (*exception DUP*)
   val join: (key -> 'a * 'a -> 'a) (*exception SAME*) ->
     'a table * 'a table -> 'a table                                    (*exception DUP*)
   val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table      (*exception DUP*)
   val delete: key -> 'a table -> 'a table                              (*exception UNDEF*)
   val delete_safe: key -> 'a table -> 'a table
   val member: ('b * 'a -> bool) -> 'a table -> key * 'b -> bool
   val insert: ('a * 'a -> bool) -> key * 'a -> 'a table -> 'a table    (*exception DUP*)
   val remove: ('b * 'a -> bool) -> key * 'b -> 'a table -> 'a table
   val lookup_list: 'a list table -> key -> 'a list
   val cons_list: key * 'a -> 'a list table -> 'a list table
   val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
   val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list table -> 'a list table
   val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list table -> 'a list table
   val make_list: (key * 'a) list -> 'a list table
   val dest_list: 'a list table -> (key * 'a) list
   val merge_list: ('a * 'a -> bool) -> 'a list table * 'a list table -> 'a list table
   type set = unit table
   val insert_set: key -> set -> set
   val remove_set: key -> set -> set
   val make_set: key list -> set
 end;
 
 functor Table(Key: KEY): TABLE =
 struct
 
+structure Key = Key;
+type key = Key.key;
 
-(* datatype table *)
 
-type key = Key.key;
+(* datatype *)
 
 datatype 'a table =
   Empty |
   Branch2 of 'a table * (key * 'a) * 'a table |
   Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table;
 
 exception DUP of key;
 
 
 (* empty and single *)
 
 val empty = Empty;
 
 fun build (f: 'a table -> 'a table) = f empty;
 
 fun is_empty Empty = true
   | is_empty _ = false;
 
 fun is_single (Branch2 (Empty, _, Empty)) = true
   | is_single _ = false;
 
 
 (* map and fold combinators *)
 
 fun map_table f =
   let
     fun map Empty = Empty
       | map (Branch2 (left, (k, x), right)) =
           Branch2 (map left, (k, f k x), map right)
       | map (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
           Branch3 (map left, (k1, f k1 x1), map mid, (k2, f k2 x2), map right);
   in map end;
 
 fun fold_table f =
   let
     fun fold Empty x = x
       | fold (Branch2 (left, e, right)) x =
           fold right (f e (fold left x))
       | fold (Branch3 (left, e1, mid, e2, right)) x =
           fold right (f e2 (fold mid (f e1 (fold left x))));
   in fold end;
 
 fun fold_rev_table f =
   let
     fun fold Empty x = x
       | fold (Branch2 (left, e, right)) x =
           fold left (f e (fold right x))
       | fold (Branch3 (left, e1, mid, e2, right)) x =
           fold left (f e1 (fold mid (f e2 (fold right x))));
   in fold end;
 
 fun dest tab = fold_rev_table cons tab [];
 fun keys tab = fold_rev_table (cons o #1) tab [];
 
 
 (* min/max entries *)
 
 fun min Empty = NONE
   | min (Branch2 (Empty, e, _)) = SOME e
   | min (Branch3 (Empty, e, _, _, _)) = SOME e
   | min (Branch2 (left, _, _)) = min left
   | min (Branch3 (left, _, _, _, _)) = min left;
 
 fun max Empty = NONE
   | max (Branch2 (_, e, Empty)) = SOME e
   | max (Branch3 (_, _, _, e, Empty)) = SOME e
   | max (Branch2 (_, _, right)) = max right
   | max (Branch3 (_, _, _, _, right)) = max right;
 
 
 (* exists and forall *)
 
 fun exists pred =
   let
     fun ex Empty = false
       | ex (Branch2 (left, e, right)) =
           ex left orelse pred e orelse ex right
       | ex (Branch3 (left, e1, mid, e2, right)) =
           ex left orelse pred e1 orelse ex mid orelse pred e2 orelse ex right;
   in ex end;
 
 fun forall pred = not o exists (not o pred);
 
 
 (* get_first *)
 
 fun get_first f =
   let
     fun get Empty = NONE
       | get (Branch2 (left, e, right)) =
           (case get left of
             NONE =>
               (case f e of
                 NONE => get right
               | some => some)
           | some => some)
       | get (Branch3 (left, e1, mid, e2, right)) =
           (case get left of
             NONE =>
               (case f e1 of
                 NONE =>
                   (case get mid of
                     NONE =>
                       (case f e2 of
                         NONE => get right
                       | some => some)
                   | some => some)
               | some => some)
           | some => some);
   in get end;
 
 
 (* lookup *)
 
 fun lookup tab key =
   let
     fun look Empty = NONE
       | look (Branch2 (left, (k, x), right)) =
           (case Key.ord (key, k) of
             LESS => look left
           | EQUAL => SOME x
           | GREATER => look right)
       | look (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
           (case Key.ord (key, k1) of
             LESS => look left
           | EQUAL => SOME x1
           | GREATER =>
               (case Key.ord (key, k2) of
                 LESS => look mid
               | EQUAL => SOME x2
               | GREATER => look right));
   in look tab end;
 
 fun lookup_key tab key =
   let
     fun look Empty = NONE
       | look (Branch2 (left, (k, x), right)) =
           (case Key.ord (key, k) of
             LESS => look left
           | EQUAL => SOME (k, x)
           | GREATER => look right)
       | look (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
           (case Key.ord (key, k1) of
             LESS => look left
           | EQUAL => SOME (k1, x1)
           | GREATER =>
               (case Key.ord (key, k2) of
                 LESS => look mid
               | EQUAL => SOME (k2, x2)
               | GREATER => look right));
   in look tab end;
 
 fun defined tab key =
   let
     fun def Empty = false
       | def (Branch2 (left, (k, x), right)) =
           (case Key.ord (key, k) of
             LESS => def left
           | EQUAL => true
           | GREATER => def right)
       | def (Branch3 (left, (k1, x1), mid, (k2, x2), right)) =
           (case Key.ord (key, k1) of
             LESS => def left
           | EQUAL => true
           | GREATER =>
               (case Key.ord (key, k2) of
                 LESS => def mid
               | EQUAL => true
               | GREATER => def right));
   in def tab end;
 
 
 (* modify *)
 
 datatype 'a growth =
   Stay of 'a table |
   Sprout of 'a table * (key * 'a) * 'a table;
 
 exception SAME;
 
 fun modify key f tab =
   let
     fun modfy Empty = Sprout (Empty, (key, f NONE), Empty)
       | modfy (Branch2 (left, p as (k, x), right)) =
           (case Key.ord (key, k) of
             LESS =>
               (case modfy left of
                 Stay left' => Stay (Branch2 (left', p, right))
               | Sprout (left1, q, left2) => Stay (Branch3 (left1, q, left2, p, right)))
           | EQUAL => Stay (Branch2 (left, (k, f (SOME x)), right))
           | GREATER =>
               (case modfy right of
                 Stay right' => Stay (Branch2 (left, p, right'))
               | Sprout (right1, q, right2) =>
                   Stay (Branch3 (left, p, right1, q, right2))))
       | modfy (Branch3 (left, p1 as (k1, x1), mid, p2 as (k2, x2), right)) =
           (case Key.ord (key, k1) of
             LESS =>
               (case modfy left of
                 Stay left' => Stay (Branch3 (left', p1, mid, p2, right))
               | Sprout (left1, q, left2) =>
                   Sprout (Branch2 (left1, q, left2), p1, Branch2 (mid, p2, right)))
           | EQUAL => Stay (Branch3 (left, (k1, f (SOME x1)), mid, p2, right))
           | GREATER =>
               (case Key.ord (key, k2) of
                 LESS =>
                   (case modfy mid of
                     Stay mid' => Stay (Branch3 (left, p1, mid', p2, right))
                   | Sprout (mid1, q, mid2) =>
                       Sprout (Branch2 (left, p1, mid1), q, Branch2 (mid2, p2, right)))
               | EQUAL => Stay (Branch3 (left, p1, mid, (k2, f (SOME x2)), right))
               | GREATER =>
                   (case modfy right of
                     Stay right' => Stay (Branch3 (left, p1, mid, p2, right'))
                   | Sprout (right1, q, right2) =>
                       Sprout (Branch2 (left, p1, mid), p2, Branch2 (right1, q, right2)))));
 
   in
     (case modfy tab of
       Stay tab' => tab'
     | Sprout br => Branch2 br)
     handle SAME => tab
   end;
 
 fun update (key, x) tab = modify key (fn _ => x) tab;
 fun update_new (key, x) tab = modify key (fn NONE => x | SOME _ => raise DUP key) tab;
 fun default (key, x) tab = modify key (fn NONE => x | SOME _ => raise SAME) tab;
 fun map_entry key f = modify key (fn NONE => raise SAME | SOME x => f x);
 fun map_default (key, x) f = modify key (fn NONE => f x | SOME y => f y);
 
 
 (* delete *)
 
 exception UNDEF of key;
 
 local
 
 fun compare NONE (k2, _) = LESS
   | compare (SOME k1) (k2, _) = Key.ord (k1, k2);
 
 fun if_eq EQUAL x y = x
   | if_eq _ x y = y;
 
 fun del (SOME k) Empty = raise UNDEF k
   | del NONE (Branch2 (Empty, p, Empty)) = (p, (true, Empty))
   | del NONE (Branch3 (Empty, p, Empty, q, Empty)) =
       (p, (false, Branch2 (Empty, q, Empty)))
   | del k (Branch2 (Empty, p, Empty)) =
       (case compare k p of
         EQUAL => (p, (true, Empty))
       | _ => raise UNDEF (the k))
   | del k (Branch3 (Empty, p, Empty, q, Empty)) =
       (case compare k p of
         EQUAL => (p, (false, Branch2 (Empty, q, Empty)))
       | _ =>
         (case compare k q of
           EQUAL => (q, (false, Branch2 (Empty, p, Empty)))
         | _ => raise UNDEF (the k)))
   | del k (Branch2 (l, p, r)) =
       (case compare k p of
         LESS =>
           (case del k l of
             (p', (false, l')) => (p', (false, Branch2 (l', p, r)))
           | (p', (true, l')) => (p', case r of
               Branch2 (rl, rp, rr) =>
                 (true, Branch3 (l', p, rl, rp, rr))
             | Branch3 (rl, rp, rm, rq, rr) => (false, Branch2
                 (Branch2 (l', p, rl), rp, Branch2 (rm, rq, rr)))))
       | ord =>
           (case del (if_eq ord NONE k) r of
             (p', (false, r')) => (p', (false, Branch2 (l, if_eq ord p' p, r')))
           | (p', (true, r')) => (p', case l of
               Branch2 (ll, lp, lr) =>
                 (true, Branch3 (ll, lp, lr, if_eq ord p' p, r'))
             | Branch3 (ll, lp, lm, lq, lr) => (false, Branch2
                 (Branch2 (ll, lp, lm), lq, Branch2 (lr, if_eq ord p' p, r'))))))
   | del k (Branch3 (l, p, m, q, r)) =
       (case compare k q of
         LESS =>
           (case compare k p of
             LESS =>
               (case del k l of
                 (p', (false, l')) => (p', (false, Branch3 (l', p, m, q, r)))
               | (p', (true, l')) => (p', (false, case (m, r) of
                   (Branch2 (ml, mp, mr), Branch2 _) =>
                     Branch2 (Branch3 (l', p, ml, mp, mr), q, r)
                 | (Branch3 (ml, mp, mm, mq, mr), _) =>
                     Branch3 (Branch2 (l', p, ml), mp, Branch2 (mm, mq, mr), q, r)
                 | (Branch2 (ml, mp, mr), Branch3 (rl, rp, rm, rq, rr)) =>
                     Branch3 (Branch2 (l', p, ml), mp, Branch2 (mr, q, rl), rp,
                       Branch2 (rm, rq, rr)))))
           | ord =>
               (case del (if_eq ord NONE k) m of
                 (p', (false, m')) =>
                   (p', (false, Branch3 (l, if_eq ord p' p, m', q, r)))
               | (p', (true, m')) => (p', (false, case (l, r) of
                   (Branch2 (ll, lp, lr), Branch2 _) =>
                     Branch2 (Branch3 (ll, lp, lr, if_eq ord p' p, m'), q, r)
                 | (Branch3 (ll, lp, lm, lq, lr), _) =>
                     Branch3 (Branch2 (ll, lp, lm), lq,
                       Branch2 (lr, if_eq ord p' p, m'), q, r)
                 | (_, Branch3 (rl, rp, rm, rq, rr)) =>
                     Branch3 (l, if_eq ord p' p, Branch2 (m', q, rl), rp,
                       Branch2 (rm, rq, rr))))))
       | ord =>
           (case del (if_eq ord NONE k) r of
             (q', (false, r')) =>
               (q', (false, Branch3 (l, p, m, if_eq ord q' q, r')))
           | (q', (true, r')) => (q', (false, case (l, m) of
               (Branch2 _, Branch2 (ml, mp, mr)) =>
                 Branch2 (l, p, Branch3 (ml, mp, mr, if_eq ord q' q, r'))
             | (_, Branch3 (ml, mp, mm, mq, mr)) =>
                 Branch3 (l, p, Branch2 (ml, mp, mm), mq,
                   Branch2 (mr, if_eq ord q' q, r'))
             | (Branch3 (ll, lp, lm, lq, lr), Branch2 (ml, mp, mr)) =>
                 Branch3 (Branch2 (ll, lp, lm), lq, Branch2 (lr, p, ml), mp,
                   Branch2 (mr, if_eq ord q' q, r'))))));
 
 in
 
 fun delete key tab = snd (snd (del (SOME key) tab));
 fun delete_safe key tab = if defined tab key then delete key tab else tab;
 
 end;
 
 
 (* membership operations *)
 
 fun member eq tab (key, x) =
   (case lookup tab key of
     NONE => false
   | SOME y => eq (x, y));
 
 fun insert eq (key, x) =
   modify key (fn NONE => x | SOME y => if eq (x, y) then raise SAME else raise DUP key);
 
 fun remove eq (key, x) tab =
   (case lookup tab key of
     NONE => tab
   | SOME y => if eq (x, y) then delete key tab else tab);
 
 
 (* simultaneous modifications *)
 
 fun make entries = build (fold update_new entries);
 
 fun join f (table1, table2) =
   let
     fun add (key, y) tab = modify key (fn NONE => y | SOME x => f key (x, y)) tab;
   in
     if pointer_eq (table1, table2) then table1
     else if is_empty table1 then table2
     else fold_table add table2 table1
   end;
 
 fun merge eq = join (fn key => fn xy => if eq xy then raise SAME else raise DUP key);
 
 
 (* list tables *)
 
 fun lookup_list tab key = these (lookup tab key);
 
 fun cons_list (key, x) tab = modify key (fn NONE => [x] | SOME xs => x :: xs) tab;
 
 fun insert_list eq (key, x) =
   modify key (fn NONE => [x] | SOME xs => if Library.member eq xs x then raise SAME else x :: xs);
 
 fun remove_list eq (key, x) tab =
   map_entry key (fn xs => (case Library.remove eq x xs of [] => raise UNDEF key | ys => ys)) tab
   handle UNDEF _ => delete key tab;
 
 fun update_list eq (key, x) =
   modify key (fn NONE => [x] | SOME [] => [x] | SOME (xs as y :: _) =>
     if eq (x, y) then raise SAME else Library.update eq x xs);
 
 fun make_list args = build (fold_rev cons_list args);
 fun dest_list tab = maps (fn (key, xs) => map (pair key) xs) (dest tab);
 fun merge_list eq = join (fn _ => Library.merge eq);
 
 
 (* set operations *)
 
 type set = unit table;
 
 fun insert_set x = default (x, ());
 fun remove_set x : set -> set = delete_safe x;
 fun make_set xs = build (fold insert_set xs);
 
 
 (* ML pretty-printing *)
 
 val _ =
   ML_system_pp (fn depth => fn pretty => fn tab =>
     ML_Pretty.to_polyml
       (ML_Pretty.enum "," "{" "}"
         (ML_Pretty.pair
           (ML_Pretty.from_polyml o ML_system_pretty)
           (ML_Pretty.from_polyml o pretty))
         (dest tab, depth)));
 
 
 (*final declarations of this structure!*)
 val map = map_table;
 val fold = fold_table;
 val fold_rev = fold_rev_table;
 
 end;
 
 structure Inttab = Table(type key = int val ord = int_ord);
 structure Symtab = Table(type key = string val ord = fast_string_ord);
 structure Symreltab = Table(type key = string * string
   val ord = prod_ord fast_string_ord fast_string_ord);
diff --git a/src/Pure/term_ord.ML b/src/Pure/term_ord.ML
--- a/src/Pure/term_ord.ML
+++ b/src/Pure/term_ord.ML
@@ -1,261 +1,261 @@
 (*  Title:      Pure/term_ord.ML
     Author:     Tobias Nipkow, TU Muenchen
     Author:     Makarius
 
 Term orderings.
 *)
 
 signature TERM_ORD =
 sig
   val fast_indexname_ord: indexname ord
   val sort_ord: sort ord
   val typ_ord: typ ord
   val fast_term_ord: term ord
   val syntax_term_ord: term ord
   val indexname_ord: indexname ord
   val tvar_ord: (indexname * sort) ord
   val var_ord: (indexname * typ) ord
   val term_ord: term ord
   val hd_ord: term ord
   val term_lpo: (term -> int) -> term ord
 end;
 
 structure Term_Ord: TERM_ORD =
 struct
 
 (* fast syntactic ordering -- tuned for inequalities *)
 
 val fast_indexname_ord =
   pointer_eq_ord (int_ord o apply2 snd ||| fast_string_ord o apply2 fst);
 
 val sort_ord =
   pointer_eq_ord (dict_ord fast_string_ord);
 
 local
 
 fun cons_nr (TVar _) = 0
   | cons_nr (TFree _) = 1
   | cons_nr (Type _) = 2;
 
 in
 
 fun typ_ord TU =
   if pointer_eq TU then EQUAL
   else
     (case TU of
       (Type (a, Ts), Type (b, Us)) =>
         (case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us) | ord => ord)
     | (TFree (a, S), TFree (b, S')) =>
         (case fast_string_ord (a, b) of EQUAL => sort_ord (S, S') | ord => ord)
     | (TVar (xi, S), TVar (yj, S')) =>
         (case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S') | ord => ord)
     | (T, U) => int_ord (cons_nr T, cons_nr U));
 
 end;
 
 local
 
 fun cons_nr (Const _) = 0
   | cons_nr (Free _) = 1
   | cons_nr (Var _) = 2
   | cons_nr (Bound _) = 3
   | cons_nr (Abs _) = 4
   | cons_nr (_ $ _) = 5;
 
 fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u)
   | struct_ord (t1 $ t2, u1 $ u2) =
       (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord)
   | struct_ord (t, u) = int_ord (cons_nr t, cons_nr u);
 
 fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u)
   | atoms_ord (t1 $ t2, u1 $ u2) =
       (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord)
   | atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b)
   | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
   | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
   | atoms_ord (Bound i, Bound j) = int_ord (i, j)
   | atoms_ord _ = EQUAL;
 
 fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
       (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
   | types_ord (t1 $ t2, u1 $ u2) =
       (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord)
   | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U)
   | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
   | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
   | types_ord _ = EQUAL;
 
 fun comments_ord (Abs (x, _, t), Abs (y, _, u)) =
       (case fast_string_ord (x, y) of EQUAL => comments_ord (t, u) | ord => ord)
   | comments_ord (t1 $ t2, u1 $ u2) =
       (case comments_ord (t1, u1) of EQUAL => comments_ord (t2, u2) | ord => ord)
   | comments_ord _ = EQUAL;
 
 in
 
 val fast_term_ord = pointer_eq_ord (struct_ord ||| atoms_ord ||| types_ord);
 
 val syntax_term_ord = fast_term_ord ||| comments_ord;
 
 end;
 
 
 (* term_ord *)
 
 (*a linear well-founded AC-compatible ordering for terms:
   s < t <=> 1. size(s) < size(t) or
             2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
             3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
                (s1..sn) < (t1..tn) (lexicographically)*)
 
 val indexname_ord = int_ord o apply2 #2 ||| string_ord o apply2 #1;
 val tvar_ord = prod_ord indexname_ord sort_ord;
 val var_ord = prod_ord indexname_ord typ_ord;
 
 
 local
 
 fun hd_depth (t $ _, n) = hd_depth (t, n + 1)
   | hd_depth p = p;
 
 fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
   | dest_hd (Free (a, T)) = (((a, 0), T), 1)
   | dest_hd (Var v) = (v, 2)
   | dest_hd (Bound i) = ((("", i), dummyT), 3)
   | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
 
 in
 
 fun term_ord tu =
   if pointer_eq tu then EQUAL
   else
     (case tu of
       (Abs (_, T, t), Abs(_, U, u)) =>
         (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
     | (t, u) =>
         (case int_ord (size_of_term t, size_of_term u) of
           EQUAL =>
             (case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of
               EQUAL => args_ord (t, u) | ord => ord)
         | ord => ord))
 and hd_ord (f, g) =
   prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
 and args_ord (f $ t, g $ u) =
       (case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord)
   | args_ord _ = EQUAL;
 
 end;
 
 
 (* Lexicographic path order on terms *)
 
 (*
   See Baader & Nipkow, Term rewriting, CUP 1998.
   Without variables.  Const, Var, Bound, Free and Abs are treated all as
   constants.
 
   f_ord maps terms to integers and serves two purposes:
   - Predicate on constant symbols.  Those that are not recognised by f_ord
     must be mapped to ~1.
   - Order on the recognised symbols.  These must be mapped to distinct
     integers >= 0.
   The argument of f_ord is never an application.
 *)
 
 local
 
 fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0)
   | unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0)
   | unrecognized (Var v) = ((1, v), 1)
   | unrecognized (Bound i) = ((1, (("", i), dummyT)), 2)
   | unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
 
 fun dest_hd f_ord t =
   let val ord = f_ord t
   in if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0) end;
 
 fun term_lpo f_ord (s, t) =
   let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
     if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
     then case hd_ord f_ord (f, g) of
         GREATER =>
           if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
           then GREATER else LESS
       | EQUAL =>
           if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
           then list_ord (term_lpo f_ord) (ss, ts)
           else LESS
       | LESS => LESS
     else GREATER
   end
 and hd_ord f_ord (f, g) = case (f, g) of
     (Abs (_, T, t), Abs (_, U, u)) =>
       (case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
   | (_, _) => prod_ord (prod_ord int_ord
                   (prod_ord indexname_ord typ_ord)) int_ord
                 (dest_hd f_ord f, dest_hd f_ord g);
 
 in
 val term_lpo = term_lpo
 end;
 
 end;
 
 
 (* scalable collections *)
 
 structure Vartab = Table(type key = indexname val ord = Term_Ord.fast_indexname_ord);
 structure Sorttab = Table(type key = sort val ord = Term_Ord.sort_ord);
 structure Typtab = Table(type key = typ val ord = Term_Ord.typ_ord);
 
 structure Termtab:
 sig
   include TABLE
   val term_cache: (term -> 'a) -> term -> 'a
 end =
 struct
 
 structure Table = Table(type key = term val ord = Term_Ord.fast_term_ord);
 open Table;
 
 fun term_cache f = Cache.create empty lookup update f;
 
 end;
 
-structure Termset = Set(type key = term val ord = Term_Ord.fast_term_ord);
+structure Termset = Set(Termtab.Key);
 
 structure Sortset:
 sig
   include SET
   val insert_typ: typ -> T -> T
   val insert_typs: typ list -> T -> T
   val insert_term: term -> T -> T
   val insert_terms: term list -> T -> T
 end =
 struct
 
-structure Set = Set(type key = sort val ord = Term_Ord.sort_ord);
+structure Set = Set(Sorttab.Key);
 open Set;
 
 fun insert_typ (TFree (_, S)) Ss = insert S Ss
   | insert_typ (TVar (_, S)) Ss = insert S Ss
   | insert_typ (Type (_, Ts)) Ss = insert_typs Ts Ss
 and insert_typs [] Ss = Ss
   | insert_typs (T :: Ts) Ss = insert_typs Ts (insert_typ T Ss);
 
 fun insert_term (Const (_, T)) Ss = insert_typ T Ss
   | insert_term (Free (_, T)) Ss = insert_typ T Ss
   | insert_term (Var (_, T)) Ss = insert_typ T Ss
   | insert_term (Bound _) Ss = Ss
   | insert_term (Abs (_, T, t)) Ss = insert_term t (insert_typ T Ss)
   | insert_term (t $ u) Ss = insert_term t (insert_term u Ss);
 
 fun insert_terms [] Ss = Ss
   | insert_terms (t :: ts) Ss = insert_terms ts (insert_term t Ss);
 
 end;
 
-structure Var_Graph = Graph(type key = indexname val ord = Term_Ord.fast_indexname_ord);
-structure Sort_Graph = Graph(type key = sort val ord = Term_Ord.sort_ord);
-structure Typ_Graph = Graph(type key = typ val ord = Term_Ord.typ_ord);
-structure Term_Graph = Graph(type key = term val ord = Term_Ord.fast_term_ord);
+structure Var_Graph = Graph(Vartab.Key);
+structure Sort_Graph = Graph(Sorttab.Key);
+structure Typ_Graph = Graph(Typtab.Key);
+structure Term_Graph = Graph(Termtab.Key);