diff -r b0de8551fadf -r c4e29a0bb8c1 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Sat Mar 06 19:17:59 2010 +0000
+++ b/src/HOL/Tools/Function/mutual.ML	Sun Mar 07 11:57:16 2010 +0100
@@ -190,7 +190,7 @@
   in
     Goal.prove ctxt [] []
       (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
-      (fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs)
+      (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)
     |> restore_cond