Nominal/NewParser.thy
changeset 2076 6cb1a4639521
parent 2048 20be95dce643
child 2089 e9f089a5cc17
--- 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