src/HOL/Import/shuffler.ML

--- a/src/HOL/Import/shuffler.ML	Wed Dec 31 00:08:14 2008 +0100
+++ b/src/HOL/Import/shuffler.ML	Wed Dec 31 15:30:10 2008 +0100
@@ -353,7 +353,7 @@
 
 fun equals_fun thy assume t =
     case t of
-        Const("op ==",_) $ u $ v => if Term.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
+        Const("op ==",_) $ u $ v => if TermOrd.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
       | _ => NONE
 
 fun eta_expand thy assumes origt =