tuned;
authorwenzelm
Thu, 23 Feb 2012 16:02:07 +0100
changeset 46615 c29bf6741ace
parent 46614 165886a4fe64
child 46616 cd0e6841ab9c
tuned;
src/Pure/General/graph.scala
--- 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 */