diff -r b0de8551fadf -r c4e29a0bb8c1 src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Sat Mar 06 19:17:59 2010 +0000
+++ b/src/HOLCF/Tools/fixrec.ML	Sun Mar 07 11:57:16 2010 +0100
@@ -146,9 +146,9 @@
     val predicate = lambda_tuple lhss (list_comb (P, lhss));
     val tuple_induct_thm = (def_cont_fix_ind OF [tuple_fixdef_thm, cont_thm])
       |> Drule.instantiate' [] [SOME (Thm.cterm_of thy predicate)]
-      |> LocalDefs.unfold lthy @{thms split_paired_all split_conv split_strict};
+      |> Local_Defs.unfold lthy @{thms split_paired_all split_conv split_strict};
     val tuple_unfold_thm = (def_cont_fix_eq OF [tuple_fixdef_thm, cont_thm])
-      |> LocalDefs.unfold lthy' @{thms split_conv};
+      |> Local_Defs.unfold lthy' @{thms split_conv};
     fun unfolds [] thm = []
       | unfolds (n::[]) thm = [(n, thm)]
       | unfolds (n::ns) thm = let