src/Pure/General/graph.ML

 
 type key = Key.key;
 
 val eq_key = equal EQUAL o Key.ord;
 
-infix mem_key;
-val op mem_key = gen_mem eq_key;
-
+val member_key = member eq_key;
 val remove_key = remove eq_key;
 
 
 (* tables and sets of keys *)
 
 structure Table = TableFun(Key);
 type keys = unit Table.table;
 
 val empty_keys = Table.empty: keys;
 
-infix mem_keys;
-fun x mem_keys tab = Table.defined (tab: keys) x;
-
-infix ins_keys;
-fun x ins_keys tab = Table.insert (K true) (x, ()) (tab: keys);
+fun member_keys tab = Table.defined (tab: keys);
+fun insert_keys x tab = Table.insert (K true) (x, ()) (tab: keys);
 
 
 (* graphs *)
 
 datatype 'a T = Graph of ('a * (key list * key list)) Table.table;

 
 (*nodes reachable from xs -- topologically sorted for acyclic graphs*)
 fun reachable next xs =
   let
     fun reach x (rs, R) =
-      if x mem_keys R then (rs, R)
-      else apfst (cons x) (fold reach (next x) (rs, x ins_keys R))
+      if member_keys R x then (rs, R)
+      else apfst (cons x) (fold reach (next x) (rs, insert_keys x R))
   in fold_map (fn x => reach x o pair []) xs empty_keys end;
 
 (*immediate*)
 fun imm_preds G = #1 o #2 o get_entry G;
 fun imm_succs G = #2 o #2 o get_entry G;

 fun find_paths G (x, y) =
   let
     val (_, X) = reachable (imm_succs G) [x];
     fun paths ps p =
       if not (null ps) andalso eq_key (p, x) then [p :: ps]
-      else if p mem_keys X andalso not (p mem_key ps)
+      else if member_keys X p andalso not (member_key ps p)
       then List.concat (map (paths (p :: ps)) (imm_preds G p))
       else [];
   in paths [] y end;
 
 

       (i, (fold remove_key xs preds, fold remove_key xs succs))));
 
 
 (* edges *)
 
-fun is_edge G (x, y) = y mem_key imm_succs G x handle UNDEF _ => false;
+fun is_edge G (x, y) = member_key (imm_succs G x) y handle UNDEF _ => false;
 
 fun add_edge (x, y) G =
   if is_edge G (x, y) then G
   else
     G |> map_entry y (fn (i, (preds, succs)) => (i, (x :: preds, succs)))