src/HOL/Tools/Function/partial_function.ML

     _ $ (_ $ Abs (_, _, body)) =>
       (case dest_case (ProofContext.theory_of ctxt) body of
          NONE => no_tac
        | SOME (arg, conv) =>
            let open Conv in
-              if not (null (loose_bnos arg)) then no_tac
+              if Term.is_open arg then no_tac
               else ((DETERM o strip_cases o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
                 THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
                 THEN_ALL_NEW etac @{thm thin_rl}
                 THEN_ALL_NEW (CONVERSION
                   (params_conv ~1 (fn ctxt' =>