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