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