diff -r ef97c5006840 -r acb789f3936b src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Sun May 09 12:00:43 2010 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Sun May 09 15:28:44 2010 +0200
@@ -192,7 +192,7 @@
       (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
       (fn _ => (Local_Defs.unfold_tac ctxt all_orig_fdefs)
          THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
-         THEN (simp_tac (simpset_of ctxt addsimps SumTree.proj_in_rules)) 1)
+         THEN (simp_tac (simpset_of ctxt)) 1) (* FIXME: global simpset?!! *)
     |> restore_cond
     |> export
   end