src/Tools/subtyping.ML
changeset 46614 165886a4fe64
parent 45935 32f769f94ea4
child 46665 919dfcdf6d8a
     1.1 --- a/src/Tools/subtyping.ML	Thu Feb 23 15:15:59 2012 +0100
     1.2 +++ b/src/Tools/subtyping.ML	Thu Feb 23 15:49:40 2012 +0100
     1.3 @@ -88,8 +88,7 @@
     1.4  
     1.5  (** utils **)
     1.6  
     1.7 -fun restrict_graph G =
     1.8 -  Graph.subgraph (fn key => if Graph.get_node G key = 0 then true else false) G;
     1.9 +fun restrict_graph G = Graph.restrict (fn x => Graph.get_node G x = 0) G;
    1.10  
    1.11  fun nameT (Type (s, [])) = s;
    1.12  fun t_of s = Type (s, []);