diff -r 980d4194a212 -r b48ab741683b src/Pure/term_ord.ML
--- a/src/Pure/term_ord.ML	Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Pure/term_ord.ML	Sat Feb 27 23:13:01 2010 +0100
@@ -29,7 +29,7 @@
   val term_cache: (term -> 'a) -> term -> 'a
 end;
 
-structure TermOrd: TERM_ORD =
+structure Term_Ord: TERM_ORD =
 struct
 
 (* fast syntactic ordering -- tuned for inequalities *)
@@ -223,11 +223,11 @@
 
 end;
 
-structure Basic_Term_Ord: BASIC_TERM_ORD = TermOrd;
+structure Basic_Term_Ord: BASIC_TERM_ORD = Term_Ord;
 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);
+structure Var_Graph = Graph(type key = indexname val ord = Term_Ord.fast_indexname_ord);
+structure Sort_Graph = Graph(type key = sort val ord = Term_Ord.sort_ord);
+structure Typ_Graph = Graph(type key = typ val ord = Term_Ord.typ_ord);
+structure Term_Graph = Graph(type key = term val ord = Term_Ord.fast_term_ord);