diff -r 1803599838a6 -r 007d3b34080f src/HOL/Tools/Function/partial_function.ML
--- a/src/HOL/Tools/Function/partial_function.ML	Mon Dec 14 10:14:19 2015 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML	Mon Dec 14 11:20:31 2015 +0100
@@ -93,7 +93,7 @@
        | SOME (arg, conv) =>
            let open Conv in
               if Term.is_open arg then no_tac
-              else ((DETERM o Method.NO_CONTEXT_TACTIC ctxt o Induct.cases_tac false [[SOME arg]] NONE [])
+              else ((DETERM o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
                 THEN_ALL_NEW (rewrite_with_asm_tac ctxt 0)
                 THEN_ALL_NEW eresolve_tac ctxt @{thms thin_rl}
                 THEN_ALL_NEW (CONVERSION