diff -r d95f39448121 -r 54b64d4ad524 src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Mutabelle/mutabelle.ML	Wed May 05 18:25:34 2010 +0200
@@ -361,7 +361,7 @@
    val t' = canonize_term t comms;
    val u' = canonize_term u comms;
  in 
-   if s mem comms andalso Term_Ord.termless (u', t')
+   if member (op =) comms s andalso Term_Ord.termless (u', t')
    then Const (s, T) $ u' $ t'
    else Const (s, T) $ t' $ u'
  end