--- a/src/HOL/Tools/Function/function_elims.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/Function/function_elims.ML Sun Dec 13 21:56:15 2015 +0100
@@ -121,7 +121,7 @@
fun prep_subgoal_tac i =
REPEAT (eresolve_tac ctxt @{thms Pair_inject} i)
- THEN Method.insert_tac (case asms_thms of thm :: thms => (thm RS sym) :: thms) i
+ THEN Method.insert_tac ctxt (case asms_thms of thm :: thms => (thm RS sym) :: thms) i
THEN propagate_tac ctxt i
THEN TRY ((EqSubst.eqsubst_asm_tac ctxt [1] psimps i) THEN assume_tac ctxt i)
THEN bool_subst_tac ctxt i;