# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273148070 -7200
# Node ID 6cb1a463952172535d75a291f4eef185750f0290
# Parent  c1edd05f207fd467460d734e3104b2539587bc4e
mem => member

diff -r c1edd05f207f -r 6cb1a4639521 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Thu May 06 14:13:45 2010 +0200
+++ b/Nominal/NewParser.thy	Thu May 06 14:14:30 2010 +0200
@@ -672,9 +672,9 @@
 fun included i bcs = 
 let
   fun incl (BEmy j) = i = j
-    | incl (BLst (bns, bds)) = (i mem (map snd bns)) orelse (i mem bds) 
-    | incl (BSet (bns, bds)) = (i mem (map snd bns)) orelse (i mem bds) 
-    | incl (BRes (bns, bds)) = (i mem (map snd bns)) orelse (i mem bds) 
+    | incl (BLst (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i)
+    | incl (BSet (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i)
+    | incl (BRes (bns, bds)) = (member (op =) (map snd bns) i) orelse (member (op =) bds i)
 in
   exists incl bcs 
 end