# HG changeset patch
# User obua
# Date 1121086375 -7200
# Node ID ea667a5426fe99624cd21afd46057277241f6a6a
# Parent  b8b1f310877f0d87857112b8c62f18d03278146a
Improved implementation of Defs.is_overloaded.

diff -r b8b1f310877f -r ea667a5426fe src/Pure/defs.ML
--- a/src/Pure/defs.ML	Fri Jul 08 11:57:15 2005 +0200
+++ b/src/Pure/defs.ML	Mon Jul 11 14:52:55 2005 +0200
@@ -667,10 +667,16 @@
         SOME (ty, map translate (Symtab.dest defnodes), state)
     end
       
-fun is_overloaded g c = 
-    case overloading_info g c of
-      NONE => false
-    | SOME (_, l, _) => length l >= 2
+exception Overloaded;
+fun is_overloaded (_, _, _, graph) c = 
+    let 
+      fun count (c, _) = if c = 1 then raise Overloaded else c+1
+    in
+      case Symtab.lookup (graph, c) of
+        NONE => false
+      | SOME (Node (_, defnodes, _, _, _)) =>
+        ((Symtab.foldl count (0, defnodes); false) handle Overloaded => true)
+    end
 
 end;