diff -r 980d4194a212 -r b48ab741683b src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Sat Feb 27 22:52:25 2010 +0100
+++ b/src/Pure/meta_simplifier.ML	Sat Feb 27 23:13:01 2010 +0100
@@ -755,7 +755,7 @@
   mk_eq_True = K NONE,
   reorient = default_reorient};
 
-val empty_ss = init_ss basic_mk_rews TermOrd.termless (K (K no_tac)) ([], []);
+val empty_ss = init_ss basic_mk_rews Term_Ord.termless (K (K no_tac)) ([], []);
 
 
 (* merge *)  (*NOTE: ignores some fields of 2nd simpset*)