Fixed small bug in print-translation for set comprehension.
--- a/Set.thy Mon Nov 28 14:42:42 1994 +0100
+++ b/Set.thy Mon Nov 28 16:45:29 1994 +0100
@@ -106,7 +106,8 @@
local
-(* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P} *)
+(* Translates between { e | x1..xn. P} and {u. ? x1..xn. u=e & P} *)
+(* {y. ? x1..xn. y = e & P} is only translated if [0..n] subset bvs(e) *)
val ex_tr = snd(mk_binder_tr("? ","Ex"));
@@ -123,8 +124,10 @@
fun setcompr_tr'[Abs(_,_,P)] =
let fun ok(Const("Ex",_)$Abs(_,_,P),n) = ok(P,n+1)
- | ok(Const("op &",_) $ (Const("op =",_) $ Bound(m) $ _) $ _, n) =
- if n>0 andalso m=n then () else raise Match
+ | 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,[]))
+ then () else raise Match
fun tr'(_ $ abs) =
let val _ $ idts $ (_ $ (_ $ _ $ e) $ Q) = ex_tr'[abs]