src/HOL/Tools/function_package/mutual.ML

 	val (mutual, thy) = analyze_eqs thy eqss
 	val Mutual {name, sum_const, qglrss, ...} = mutual
 	val global_glrs = flat qglrss
 	val used = fold (fn (qs, _, _, _) => fold (curry op ins_string o fst o dest_Free) qs) global_glrs []
     in
-	(mutual, name, FundefPrep.prepare_fundef_new thy congs name (Const sum_const) global_glrs used)
+	(mutual, name, FundefPrep.prepare_fundef thy congs name (Const sum_const) global_glrs used)
     end
 
 
 (* Beta-reduce both sides of a meta-equality *)
 fun beta_norm_eq thm =