# HG changeset patch
# User nipkow
# Date 786037529 -3600
# Node ID ec175b039523bcc9d60ef6de78bdcbe9d922bc07
# Parent  5505c746fff77bab29335778ec52f804e8d9d18f
Fixed small bug in print-translation for set comprehension.

diff -r 5505c746fff7 -r ec175b039523 Set.thy
--- 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]