--- a/src/Pure/General/graph.scala Thu Feb 23 15:49:40 2012 +0100
+++ b/src/Pure/General/graph.scala Thu Feb 23 16:02:07 2012 +0100
@@ -51,14 +51,14 @@
/* nodes */
- def map_nodes[B](f: A => B): Graph[Key, B] =
- new Graph[Key, B](rep mapValues { case (i, ps) => (f(i), ps) })
-
def get_node(x: Key): A = get_entry(x)._1
def map_node(x: Key, f: A => A): Graph[Key, A] =
map_entry(x, { case (i, ps) => (f(i), ps) })
+ def map_nodes[B](f: A => B): Graph[Key, B] =
+ new Graph[Key, B](rep mapValues { case (i, ps) => (f(i), ps) })
+
/* reachability */