diff -r 6aefc5ff8e63 -r 5c25a2012975 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/meta_simplifier.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -1,6 +1,5 @@
 (*  Title:      Pure/meta_simplifier.ML
-    ID:         $Id$
-    Author:     Tobias Nipkow and Stefan Berghofer
+    Author:     Tobias Nipkow and Stefan Berghofer, TU Muenchen
 
 Meta-level Simplification.
 *)
@@ -788,7 +787,7 @@
   mk_eq_True = K NONE,
   reorient = default_reorient};
 
-val empty_ss = init_ss basic_mk_rews Term.termless (K (K no_tac)) ([], []);
+val empty_ss = init_ss basic_mk_rews TermOrd.termless (K (K no_tac)) ([], []);
 
 
 (* merge *)  (*NOTE: ignores some fields of 2nd simpset*)