--- a/Nominal-General/nominal_permeq.ML Thu May 06 13:25:37 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML Thu May 06 14:09:21 2010 +0200
@@ -117,7 +117,7 @@
let
val hd = head_of trm
in
- if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then ()
+ if is_Const hd andalso member (op =) bad_hds (fst (dest_Const hd)) then ()
else (if strict_flag then error else warning)
("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
end
@@ -183,4 +183,4 @@
fun perm_strict_simp_meth (thms, consts) ctxt =
SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts))
-end; (* structure *)
\ No newline at end of file
+end; (* structure *)