src/HOL/Import/shuffler.ML

--- a/src/HOL/Import/shuffler.ML	Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Import/shuffler.ML	Sat Feb 27 23:13:01 2010 +0100
@@ -351,7 +351,7 @@
 
 fun equals_fun thy assume t =
     case t of
-        Const("op ==",_) $ u $ v => if TermOrd.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
+        Const("op ==",_) $ u $ v => if Term_Ord.term_ord (u,v) = LESS then SOME (meta_sym_rew) else NONE
       | _ => NONE
 
 fun eta_expand thy assumes origt =