src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML

     val flat_fs' = map_args flat_fs;
   in
     permute_like (op aconv) flat_fs fs flat_fs'
   end;
 
-fun massage_indirect_rec_call ctxt has_call massage_unapplied_direct_call bound_Ts y y' =
+fun massage_indirect_rec_call ctxt has_call raw_massage_fun bound_Ts y y' =
   let
     val typof = curry fastype_of1 bound_Ts;
     val build_map_fst = build_map ctxt (fst_const o fst);
 
     val yT = typof y;
     val yU = typof y';
 
     fun y_of_y' () = build_map_fst (yU, yT) $ y';
     val elim_y = Term.map_aterms (fn t => if t = y then y_of_y' () else t);
 
-    fun check_and_massage_unapplied_direct_call U T t =
-      if has_call t then
-        factor_out_types ctxt massage_unapplied_direct_call HOLogic.dest_prodT U T t
-      else
-        HOLogic.mk_comp (t, build_map_fst (U, T));
+    fun massage_direct_fun U T t =
+      if has_call t then factor_out_types ctxt raw_massage_fun HOLogic.dest_prodT U T t
+      else HOLogic.mk_comp (t, build_map_fst (U, T));
 
     fun massage_map (Type (_, Us)) (Type (s, Ts)) t =
         (case try (dest_map ctxt s) t of
           SOME (map0, fs) =>
           let

     and massage_map_or_map_arg U T t =
       if T = U then
         if has_call t then unexpected_rec_call ctxt t else t
       else
         massage_map U T t
-        handle AINT_NO_MAP _ => check_and_massage_unapplied_direct_call U T t;
+        handle AINT_NO_MAP _ => massage_direct_fun U T t;
 
     fun massage_call (t as t1 $ t2) =
         if t2 = y then
           massage_map yU yT (elim_y t1) $ y'
           handle AINT_NO_MAP t' => invalid_map ctxt t'

       | _ => f t)
   in
     fld
   end;
 
-fun massage_direct_corec_call ctxt has_call massage_direct_call U t =
-  massage_let_and_if ctxt has_call massage_direct_call U t;
-
-fun massage_indirect_corec_call ctxt has_call massage_direct_call bound_Ts U t =
+fun massage_direct_corec_call ctxt has_call raw_massage_call U t =
+  massage_let_and_if ctxt has_call raw_massage_call U t;
+
+fun massage_indirect_corec_call ctxt has_call raw_massage_call bound_Ts U t =
   let
     val typof = curry fastype_of1 bound_Ts;
     val build_map_Inl = build_map ctxt (uncurry Inl_const o dest_sumT o snd)
 
-    fun check_and_massage_direct_call U T t =
-      if has_call t then factor_out_types ctxt massage_direct_call dest_sumT U T t
+    fun massage_direct_call U T t =
+      if has_call t then factor_out_types ctxt raw_massage_call dest_sumT U T t
       else build_map_Inl (T, U) $ t;
 
-    fun check_and_massage_unapplied_direct_call U T t =
+    fun massage_direct_fun U T t =
       let val var = Var ((Name.uu, Term.maxidx_of_term t + 1), domain_type (typof t)) in
-        Term.lambda var (check_and_massage_direct_call U T (t $ var))
+        Term.lambda var (massage_direct_call U T (t $ var))
       end;
 
     fun massage_map (Type (_, Us)) (Type (s, Ts)) t =
         (case try (dest_map ctxt s) t of
           SOME (map0, fs) =>

     and massage_map_or_map_arg U T t =
       if T = U then
         if has_call t then unexpected_corec_call ctxt t else t
       else
         massage_map U T t
-        handle AINT_NO_MAP _ => check_and_massage_unapplied_direct_call U T t;
+        handle AINT_NO_MAP _ => massage_direct_fun U T t;
 
     fun massage_call U T =
       massage_let_and_if ctxt has_call (fn t =>
         if has_call t then
           (case U of

               end
             | NONE =>
               (case t of
                 t1 $ t2 =>
                 (if has_call t2 then
-                  check_and_massage_direct_call U T t
+                  massage_direct_call U T t
                 else
                   massage_map U T t1 $ t2
-                  handle AINT_NO_MAP _ => check_and_massage_direct_call U T t)
+                  handle AINT_NO_MAP _ => massage_direct_call U T t)
               | Abs (s, T', t') => Abs (s, T', massage_call (range_type U) (range_type T) t')
-              | _ => check_and_massage_direct_call U T t))
+              | _ => massage_direct_call U T t))
           | _ => ill_formed_corec_call ctxt t)
         else
           build_map_Inl (T, U) $ t) U
   in
     massage_call U (typof t) t