src/Pure/Isar/specification.ML

--- a/src/Pure/Isar/specification.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/Pure/Isar/specification.ML	Thu Mar 24 16:56:19 2011 +0100
@@ -107,7 +107,7 @@
       | abs_body _ _ a = a;
     fun close (y, U) B =
       let val B' = abs_body 0 y (Term.incr_boundvars 1 B)
-      in if Term.loose_bvar1 (B', 0) then Term.all dummyT $ Abs (y, U, B') else B end;
+      in if Term.is_dependent B' then Term.all dummyT $ Abs (y, U, B') else B end;
     fun close_form A =
       let
         val occ_frees = rev (fold_aterms add_free A []);