Improved implementation of Defs.is_overloaded.
authorobua
Mon Jul 11 14:52:55 2005 +0200 (2005-07-11)
changeset 16766ea667a5426fe
parent 16765 b8b1f310877f
child 16767 2d4433759b8d
Improved implementation of Defs.is_overloaded.
src/Pure/defs.ML
     1.1 --- a/src/Pure/defs.ML	Fri Jul 08 11:57:15 2005 +0200
     1.2 +++ b/src/Pure/defs.ML	Mon Jul 11 14:52:55 2005 +0200
     1.3 @@ -667,10 +667,16 @@
     1.4          SOME (ty, map translate (Symtab.dest defnodes), state)
     1.5      end
     1.6        
     1.7 -fun is_overloaded g c = 
     1.8 -    case overloading_info g c of
     1.9 -      NONE => false
    1.10 -    | SOME (_, l, _) => length l >= 2
    1.11 +exception Overloaded;
    1.12 +fun is_overloaded (_, _, _, graph) c = 
    1.13 +    let 
    1.14 +      fun count (c, _) = if c = 1 then raise Overloaded else c+1
    1.15 +    in
    1.16 +      case Symtab.lookup (graph, c) of
    1.17 +        NONE => false
    1.18 +      | SOME (Node (_, defnodes, _, _, _)) =>
    1.19 +        ((Symtab.foldl count (0, defnodes); false) handle Overloaded => true)
    1.20 +    end
    1.21  
    1.22  end;
    1.23