src/HOL/Set.thy
changeset 10985 65a8a0e2d55b
parent 10832 e33b47e4246d
child 11752 8941d8d15dc8
--- a/src/HOL/Set.thy	Fri Jan 26 15:50:52 2001 +0100
+++ b/src/HOL/Set.thy	Sun Jan 28 16:46:19 2001 +0100
@@ -184,9 +184,9 @@
 
 fun setcompr_tr'[Abs(_,_,P)] =
   let fun ok(Const("Ex",_)$Abs(_,_,P),n) = ok(P,n+1)
-        | ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ e) $ _, n) =
-            if n>0 andalso m=n andalso
-              ((0 upto (n-1)) subset add_loose_bnos(e,0,[]))
+        | ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ e) $ P, n) =
+            if n>0 andalso m=n andalso not(loose_bvar1(P,n)) andalso
+               ((0 upto (n-1)) subset add_loose_bnos(e,0,[]))
             then () else raise Match
 
       fun tr'(_ $ abs) =