src/Pure/consts.ML

--- a/src/Pure/consts.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/Pure/consts.ML	Thu Mar 24 16:56:19 2011 +0100
@@ -255,7 +255,7 @@
 local
 
 fun strip_abss (t as Abs (x, T, b)) =
-      if Term.loose_bvar1 (b, 0) then strip_abss b |>> cons (x, T)
+      if Term.is_dependent b then strip_abss b |>> cons (x, T)  (* FIXME decr!? *)
       else ([], t)
   | strip_abss t = ([], t);