--- 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
--- 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) =