--- a/src/Pure/term_ord.ML Sat Feb 27 21:56:05 2010 +0100
+++ b/src/Pure/term_ord.ML Sat Feb 27 21:56:55 2010 +0100
@@ -226,3 +226,6 @@
structure Basic_Term_Ord: BASIC_TERM_ORD = TermOrd;
open Basic_Term_Ord;
+
+structure Term_Graph = Graph(type key = term val ord = TermOrd.fast_term_ord);
+