Nominal-General/nominal_eqvt.ML
changeset 2069 2b6ba4d4e19a
parent 2064 2725853f43b9
child 2081 9e7cf0a996d3
--- a/Nominal-General/nominal_eqvt.ML	Thu May 06 13:25:37 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML	Thu May 06 14:09:21 2010 +0200
@@ -77,7 +77,7 @@
 let
   fun split_conj names (Const ("op &", _) $ f1 $ f2) = 
       (case head_of f1 of
-         Const (name, _) => if name mem names then SOME f2 else NONE
+         Const (name, _) => if member (op =) names name then SOME f2 else NONE
        | _ => NONE)
   | split_conj _ _ = NONE;
 in
@@ -178,4 +178,4 @@
       K.thy_decl (P.xname >> equivariance);
 end;
 
-end (* structure *)
\ No newline at end of file
+end (* structure *)