# HG changeset patch
# User wenzelm
# Date 1267307526 -3600
# Node ID 1f1a1987428a51c0c4fda271366fe0a15bd2bf09
# Parent  fc130c5e81ecc7915a25c3170677c17a42cf652a
further standard instances of functor Graph;

diff -r fc130c5e81ec -r 1f1a1987428a src/Pure/term_ord.ML
--- a/src/Pure/term_ord.ML	Sat Feb 27 22:41:22 2010 +0100
+++ b/src/Pure/term_ord.ML	Sat Feb 27 22:52:06 2010 +0100
@@ -226,6 +226,8 @@
 structure Basic_Term_Ord: BASIC_TERM_ORD = TermOrd;
 open Basic_Term_Ord;
 
-
+structure Var_Graph = Graph(type key = indexname val ord = TermOrd.fast_indexname_ord);
+structure Sort_Graph = Graph(type key = sort val ord = TermOrd.sort_ord);
+structure Typ_Graph = Graph(type key = typ val ord = TermOrd.typ_ord);
 structure Term_Graph = Graph(type key = term val ord = TermOrd.fast_term_ord);