src/HOL/Mutabelle/mutabelle.ML

--- a/src/HOL/Mutabelle/mutabelle.ML	Sat Feb 27 22:52:25 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Sat Feb 27 23:13:01 2010 +0100
@@ -361,7 +361,7 @@
    val t' = canonize_term t comms;
    val u' = canonize_term u comms;
  in 
-   if s mem comms andalso TermOrd.termless (u', t')
+   if s mem comms andalso Term_Ord.termless (u', t')
    then Const (s, T) $ u' $ t'
    else Const (s, T) $ t' $ u'
  end