src/Pure/term_ord.ML
changeset 35404 de56579ae229
parent 32841 57dcddf81b01
child 35406 1f1a1987428a
     1.1 --- a/src/Pure/term_ord.ML	Sat Feb 27 21:56:05 2010 +0100
     1.2 +++ b/src/Pure/term_ord.ML	Sat Feb 27 21:56:55 2010 +0100
     1.3 @@ -226,3 +226,6 @@
     1.4  structure Basic_Term_Ord: BASIC_TERM_ORD = TermOrd;
     1.5  open Basic_Term_Ord;
     1.6  
     1.7 +
     1.8 +structure Term_Graph = Graph(type key = term val ord = TermOrd.fast_term_ord);
     1.9 +