diff -r a3793600cb93 -r 4d3527b94f2a src/HOL/Tools/Function/function_elims.ML
--- 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;