diff -r 2c57fc1f7a8c -r da70ab8531f4 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Fri Jan 10 17:44:41 2014 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Fri Jan 10 21:37:28 2014 +0100
@@ -187,8 +187,7 @@
       | [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))
+    val simp_ctxt = fold Thm.declare_hyps (#hyps (Thm.crep_thm simp)) ctxt
   in
     Goal.prove simp_ctxt [] []
       (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))