diff -r d36c7dc40000 -r eae6549dbea2 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Fri May 27 20:23:55 2016 +0200
@@ -186,7 +186,7 @@
     Goal.prove simp_ctxt [] []
       (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
       (fn _ =>
-        Local_Defs.unfold_tac ctxt all_orig_fdefs
+        Local_Defs.unfold0_tac ctxt all_orig_fdefs
           THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
           THEN (simp_tac ctxt) 1)
     |> restore_cond