diff -r 0fa87bd86566 -r f0b11413f1c9 src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Thu Feb 01 15:12:57 2018 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Thu Feb 01 15:31:25 2018 +0100
@@ -283,7 +283,7 @@
    val t' = canonize_term t comms;
    val u' = canonize_term u comms;
  in 
-   if member (op =) comms s andalso Term_Ord.termless (u', t')
+   if member (op =) comms s andalso is_less (Term_Ord.term_ord (u', t'))
    then Const (s, T) $ u' $ t'
    else Const (s, T) $ t' $ u'
  end