# HG changeset patch
# User nipkow
# Date 980696779 -3600
# Node ID 65a8a0e2d55bc876b91ef4120abfdfff1b42190f
# Parent  8f49dcbec8596c95b54844f1d4b41ee627d09977
fixed set comprehension print translation

diff -r 8f49dcbec859 -r 65a8a0e2d55b src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Jan 26 15:50:52 2001 +0100
+++ b/src/HOL/IsaMakefile	Sun Jan 28 16:46:19 2001 +0100
@@ -182,7 +182,7 @@
   Library/Quotient.thy Library/Ring_and_Field.thy \
   Library/Ring_and_Field_Example.thy Library/README.html \
   Library/Nested_Environment.thy Library/Rational_Numbers.thy Library/ROOT.ML \
-  Library/While_Combinator.thy Library/While_Combinator_Example.thy
+  Library/While_Combinator.thy
 	@$(ISATOOL) usedir $(OUT)/HOL Library
 
 
diff -r 8f49dcbec859 -r 65a8a0e2d55b src/HOL/Set.thy
--- 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) =