src/HOL/Tools/Function/partial_function.ML

--- a/src/HOL/Tools/Function/partial_function.ML	Thu Mar 24 16:47:24 2011 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Thu Mar 24 16:56:19 2011 +0100
@@ -87,7 +87,7 @@
          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}