src/Pure/General/graph.ML
changeset 31971 8c1b845ed105
parent 31616 63893e3a50a6
child 32709 c5956b54a460
     1.1 --- a/src/Pure/General/graph.ML	Thu Jul 09 17:34:59 2009 +0200
     1.2 +++ b/src/Pure/General/graph.ML	Thu Jul 09 22:01:41 2009 +0200
     1.3 @@ -52,7 +52,7 @@
     1.4    val extend: (key -> 'a * key list) -> key -> 'a T -> 'a T
     1.5  end;
     1.6  
     1.7 -functor GraphFun(Key: KEY): GRAPH =
     1.8 +functor Graph(Key: KEY): GRAPH =
     1.9  struct
    1.10  
    1.11  (* keys *)
    1.12 @@ -67,7 +67,7 @@
    1.13  
    1.14  (* tables and sets of keys *)
    1.15  
    1.16 -structure Table = TableFun(Key);
    1.17 +structure Table = Table(Key);
    1.18  type keys = unit Table.table;
    1.19  
    1.20  val empty_keys = Table.empty: keys;
    1.21 @@ -299,5 +299,5 @@
    1.22  
    1.23  end;
    1.24  
    1.25 -structure Graph = GraphFun(type key = string val ord = fast_string_ord);
    1.26 -structure IntGraph = GraphFun(type key = int val ord = int_ord);
    1.27 +structure Graph = Graph(type key = string val ord = fast_string_ord);
    1.28 +structure IntGraph = Graph(type key = int val ord = int_ord);