# HG changeset patch
# User wenzelm
# Date 1279636968 -7200
# Node ID 26906cacbaae5f51778ecd6dc192808c00eb60ef
# Parent  a902f158b4fc8c467e7608503940394399af304a
export Graph.get_entry for convenience;

diff -r a902f158b4fc -r 26906cacbaae src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Tue Jul 20 14:44:33 2010 +0200
+++ b/src/Pure/General/graph.ML	Tue Jul 20 16:42:48 2010 +0200
@@ -20,6 +20,7 @@
   val minimals: 'a T -> key list
   val maximals: 'a T -> key list
   val subgraph: (key -> bool) -> 'a T -> 'a T
+  val get_entry: 'a T -> key -> 'a * (key list * key list)            (*exception UNDEF*)
   val map_nodes: ('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