further standard instances of functor Graph;
authorwenzelm
Sat Feb 27 22:52:06 2010 +0100 (2010-02-27)
changeset 354061f1a1987428a
parent 35405 fc130c5e81ec
child 35407 980d4194a212
further standard instances of functor Graph;
src/Pure/term_ord.ML
     1.1 --- a/src/Pure/term_ord.ML	Sat Feb 27 22:41:22 2010 +0100
     1.2 +++ b/src/Pure/term_ord.ML	Sat Feb 27 22:52:06 2010 +0100
     1.3 @@ -226,6 +226,8 @@
     1.4  structure Basic_Term_Ord: BASIC_TERM_ORD = TermOrd;
     1.5  open Basic_Term_Ord;
     1.6  
     1.7 -
     1.8 +structure Var_Graph = Graph(type key = indexname val ord = TermOrd.fast_indexname_ord);
     1.9 +structure Sort_Graph = Graph(type key = sort val ord = TermOrd.sort_ord);
    1.10 +structure Typ_Graph = Graph(type key = typ val ord = TermOrd.typ_ord);
    1.11  structure Term_Graph = Graph(type key = term val ord = TermOrd.fast_term_ord);
    1.12