Improved implementation of Defs.is_overloaded.

--- 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;