# HG changeset patch
# User wenzelm
# Date 1343912732 -7200
# Node ID f13eeeea1a69be87a73ba5906dff48efc3b533ca
# Parent  a5144c4c26a2e0d9979295bf0342921ae127471e
tuned;

diff -r a5144c4c26a2 -r f13eeeea1a69 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Thu Aug 02 13:37:58 2012 +0200
+++ b/src/Pure/General/graph.scala	Thu Aug 02 15:05:32 2012 +0200
@@ -124,15 +124,12 @@
 
   def new_node(x: Key, info: A): Graph[Key, A] =
   {
-    if (rep.isDefinedAt(x)) throw new Graph.Duplicate(x)
+    if (defined(x)) throw new Graph.Duplicate(x)
     else new Graph[Key, A](rep + (x -> (info, (empty_keys, empty_keys))))
   }
 
   def default_node(x: Key, info: A): Graph[Key, A] =
-  {
-    if (rep.isDefinedAt(x)) this
-    else new_node(x, info)
-  }
+    if (defined(x)) this else new_node(x, info)
 
   private def del_adjacent(fst: Boolean, x: Key)(map: SortedMap[Key, Entry], y: Key)
       : SortedMap[Key, Entry] =