src/HOL/Mutabelle/mutabelle.ML
changeset 36692 54b64d4ad524
parent 36610 bafd82950e24
child 36743 ce2297415b54
     1.1 --- a/src/HOL/Mutabelle/mutabelle.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Mutabelle/mutabelle.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -361,7 +361,7 @@
     1.4     val t' = canonize_term t comms;
     1.5     val u' = canonize_term u comms;
     1.6   in 
     1.7 -   if s mem comms andalso Term_Ord.termless (u', t')
     1.8 +   if member (op =) comms s andalso Term_Ord.termless (u', t')
     1.9     then Const (s, T) $ u' $ t'
    1.10     else Const (s, T) $ t' $ u'
    1.11   end