diff -r 47f8bfe0f597 -r e1209fc7ecdc src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Thu Mar 24 16:56:19 2011 +0100
@@ -40,7 +40,7 @@
              (case try (HOLogic.strip_ptuple ps) q of
                 NONE => NONE
               | SOME ts =>
-                  if not (loose_bvar (S', 0)) andalso
+                  if not (Term.is_open S') andalso
                     ts = map Bound (length ps downto 0)
                   then
                     let val simp = full_simp_tac (Simplifier.inherit_context ss
@@ -128,7 +128,7 @@
     fun eta b (Abs (a, T, body)) =
           (case eta b body of
              body' as (f $ Bound 0) =>
-               if loose_bvar1 (f, 0) orelse not b then Abs (a, T, body')
+               if Term.is_dependent f orelse not b then Abs (a, T, body')
                else incr_boundvars ~1 f
            | body' => Abs (a, T, body'))
       | eta b (t $ u) = eta b t $ eta (p (head_of t)) u