--- a/src/HOL/Decision_Procs/cooper_tac.ML Thu Mar 24 16:47:24 2011 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Thu Mar 24 16:56:19 2011 +0100
@@ -46,7 +46,7 @@
val hs = map HOLogic.dest_Trueprop (Logic.strip_assums_hyp fm)
val c = HOLogic.dest_Trueprop (Logic.strip_assums_concl fm)
fun mk_all ((s, T), (P,n)) =
- if member (op =) (loose_bnos P) 0 then
+ if Term.is_dependent P then
(HOLogic.all_const T $ Abs (s, T, P), n)
else (incr_boundvars ~1 P, n-1)
fun mk_all2 (v, t) = HOLogic.all_const (fastype_of v) $ lambda v t;