# HG changeset patch
# User wenzelm
# Date 1220984550 -7200
# Node ID 7d51034545208756e2f24217a5edfe6784c6b58e
# Parent  bfd7a87006761868443c03338103f05f4bab097c
export get_first from underlying table;

diff -r bfd7a8700676 -r 7d5103454520 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Tue Sep 09 19:57:54 2008 +0200
+++ b/src/Pure/General/graph.ML	Tue Sep 09 20:22:30 2008 +0200
@@ -15,6 +15,7 @@
   val empty: 'a T
   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
@@ -85,6 +86,7 @@
 fun keys (Graph tab) = Table.keys tab;
 fun dest (Graph tab) = map (fn (x, (_, (_, succs))) => (x, 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 [];