# HG changeset patch
# User wenzelm
# Date 1330022105 -3600
# Node ID bce24d3f29e7e8bea6c97cdd8453646539c5da93
# Parent  3ccecb301d4e23e9d9b5c621edec5ebfca58aa5e
tuned -- avoid copy of empty value;

diff -r 3ccecb301d4e -r bce24d3f29e7 src/Pure/General/graph.scala
--- 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]]
 }