generalized code a bit

--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Apr 10 14:03:18 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML	Fri Apr 10 14:44:08 2015 +0200
@@ -9,7 +9,7 @@
 signature BNF_LFP_REC_SUGAR_MORE =
 sig
   val massage_nested_rec_call: Proof.context -> (term -> bool) -> (typ -> typ -> term -> term) ->
-    typ list -> term -> term -> term -> term
+    (typ * typ -> term) -> typ list -> term -> term -> term -> term
 end;
 
 structure BNF_LFP_Rec_Sugar_More : BNF_LFP_REC_SUGAR_MORE =
@@ -77,17 +77,17 @@
 fun unexpected_rec_call ctxt eqns t =
   error_at ctxt eqns ("Unexpected recursive call in " ^ quote (Syntax.string_of_term ctxt t));
 
-fun massage_nested_rec_call ctxt has_call massage_fun bound_Ts y y' t0 =
+fun massage_nested_rec_call ctxt has_call massage_fun massage_nonfun bound_Ts y y' t0 =
   let
     fun check_no_call t = if has_call t then unexpected_rec_call ctxt [t0] t else ();
 
     val typof = curry fastype_of1 bound_Ts;
-    val build_map_fst = build_map ctxt [] (fst_const o fst);
+    val massage_no_call = build_map ctxt [] massage_nonfun;
 
     val yT = typof y;
     val yU = typof y';
 
-    fun y_of_y' () = build_map_fst (yU, yT) $ y';
+    fun y_of_y' () = massage_no_call (yU, yT) $ y';
     val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t);
 
     fun massage_mutual_fun U T t =
@@ -95,7 +95,7 @@
         Const (@{const_name comp}, _) $ t1 $ t2 =>
         mk_comp bound_Ts (tap check_no_call t1, massage_mutual_fun U T t2)
       | _ =>
-        if has_call t then massage_fun U T t else mk_comp bound_Ts (t, build_map_fst (U, T)));
+        if has_call t then massage_fun U T t else mk_comp bound_Ts (t, massage_no_call (U, T)));
 
     fun massage_map (Type (_, Us)) (Type (s, Ts)) t =
         (case try (dest_map ctxt s) t of
@@ -168,7 +168,7 @@
   end;
 
 fun rewrite_nested_rec_call ctxt has_call get_ctr_pos =
-  massage_nested_rec_call ctxt has_call (rewrite_map_fun ctxt get_ctr_pos);
+  massage_nested_rec_call ctxt has_call (rewrite_map_fun ctxt get_ctr_pos) (fst_const o fst);
 
 val _ = Theory.setup (register_lfp_rec_extension
   {nested_simps = nested_simps, is_new_datatype = is_new_datatype,