more accurate goal context;

--- a/src/HOL/Tools/Function/mutual.ML	Sat Nov 23 17:07:11 2013 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Sat Nov 23 17:07:36 2013 +0100
@@ -187,8 +187,10 @@
       | [cond] => (Thm.implies_elim psimp (Thm.assume cond), Thm.implies_intr cond)
       | _ => raise General.Fail "Too many conditions"
 
+    val (_, simp_ctxt) = ctxt
+      |> Assumption.add_assumes (#hyps (Thm.crep_thm simp))
   in
-    Goal.prove ctxt [] []
+    Goal.prove simp_ctxt [] []
       (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
       (fn _ =>
         Local_Defs.unfold_tac ctxt all_orig_fdefs

--- a/src/Pure/Isar/expression.ML	Sat Nov 23 17:07:11 2013 +0100
+++ b/src/Pure/Isar/expression.ML	Sat Nov 23 17:07:36 2013 +0100
@@ -676,8 +676,11 @@
     val conjuncts =
       (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule [pred_def] (Thm.assume (cert statement))])
       |> Conjunction.elim_balanced (length ts);
+
+    val (_, axioms_ctxt) = defs_ctxt
+      |> Assumption.add_assumes (maps (#hyps o Thm.crep_thm) (defs @ conjuncts));
     val axioms = ts ~~ conjuncts |> map (fn (t, ax) =>
-      Element.prove_witness defs_ctxt t
+      Element.prove_witness axioms_ctxt t
        (rewrite_goals_tac defs THEN compose_tac (false, ax, 0) 1));
   in ((statement, intro, axioms), defs_thy) end;