--- a/src/HOL/Tools/Function/partial_function.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/Function/partial_function.ML Sun Dec 13 21:56:15 2015 +0100
@@ -62,8 +62,6 @@
(*** Automated monotonicity proofs ***)
-fun strip_cases ctac = ctac #> Seq.map snd;
-
(*rewrite conclusion with k-th assumtion*)
fun rewrite_with_asm_tac ctxt k =
Subgoal.FOCUS (fn {context = ctxt', prems, ...} =>
@@ -95,7 +93,7 @@
| SOME (arg, conv) =>
let open Conv in
if Term.is_open arg then no_tac
- else ((DETERM o strip_cases o Induct.cases_tac ctxt false [[SOME arg]] NONE [])
+ else ((DETERM o Method.NO_CONTEXT_TACTIC ctxt o Induct.cases_tac 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