# HG changeset patch
# User wenzelm
# Date 1330009327 -3600
# Node ID c29bf6741acea7866b355e8948b683d8d5a4dd0d
# Parent  165886a4fe648cff0e097878bdc650a6a902a36e
tuned;

diff -r 165886a4fe64 -r c29bf6741ace 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 */