tuned -- avoid copy of empty value;

--- a/src/Pure/General/graph.scala	Thu Feb 23 19:34:48 2012 +0100
+++ b/src/Pure/General/graph.scala	Thu Feb 23 19:35:05 2012 +0100
@@ -17,7 +17,8 @@
   class Undefined[Key](x: Key) extends Exception
   class Cycles[Key](cycles: List[List[Key]]) extends Exception
 
-  def empty[Key, A]: Graph[Key, A] = new Graph[Key, A](Map.empty)
+  private val empty_val: Graph[Any, Nothing] = new Graph[Any, Nothing](Map.empty)
+  def empty[Key, A]: Graph[Key, A] = empty_val.asInstanceOf[Graph[Key, A]]
 }