src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML

     fp_co_induct_sugar = {co_rec = recx, co_rec_thms = rec_thms, ...}, ...} : fp_sugar) =
   {T = T, fp_res_index = fp_res_index, C = C, fun_arg_Tsss = fun_arg_Tsss, ctr_sugar = ctr_sugar,
    recx = recx, rec_thms = rec_thms};
 
 fun basic_lfp_sugars_of _ [@{typ nat}] _ _ lthy =
-    ([], [0], [nat_basic_lfp_sugar], [], [], TrueI (*dummy*), [], false, lthy)
+    ([], [0], [nat_basic_lfp_sugar], [], [], [], TrueI (*dummy*), [], false, lthy)
   | basic_lfp_sugars_of bs arg_Ts callers callssss0 lthy0 =
     let
       val ((missing_arg_Ts, perm0_kks,
             fp_sugars as {fp_nesting_bnfs,
               fp_co_induct_sugar = {common_co_inducts = [common_induct], ...}, ...} :: _,

       val ctrXs_Tsss = map (#ctrXs_Tss o #fp_ctr_sugar) fp_sugars;
       val fun_arg_Tssss = map (map (map zip_XrecT)) ctrXs_Tsss;
 
       val fp_nesting_map_ident0s = map map_ident0_of_bnf fp_nesting_bnfs;
       val fp_nesting_map_comps = map map_comp_of_bnf fp_nesting_bnfs;
+      val fp_nesting_pred_maps = map pred_map_of_bnf fp_nesting_bnfs;
     in
       (missing_arg_Ts, perm0_kks, @{map 3} basic_lfp_sugar_of Cs fun_arg_Tssss fp_sugars,
-       fp_nesting_map_ident0s, fp_nesting_map_comps, common_induct, induct_attrs,
-       is_some lfp_sugar_thms, lthy)
+       fp_nesting_map_ident0s, fp_nesting_map_comps, fp_nesting_pred_maps, common_induct,
+       induct_attrs, is_some lfp_sugar_thms, lthy)
     end;
 
 exception NO_MAP of term;
 
 fun ill_formed_rec_call ctxt t =

             val map' = mk_map (length fs) Us ran_Ts map0;
             val fs' = map_flattened_map_args ctxt s (@{map 3} massage_map_or_map_arg Us Ts) fs;
           in
             Term.list_comb (map', fs')
           end
-        | NONE => raise NO_MAP t)
+        | NONE =>
+          (case try (dest_pred ctxt s) t of
+            SOME (pred0, fs) =>
+            let
+              val pred' = mk_pred Us pred0;
+              val fs' = map_flattened_map_args ctxt s (@{map 3} massage_map_or_map_arg Us Ts) fs;
+            in
+              Term.list_comb (pred', fs')
+            end
+          | NONE => raise NO_MAP t))
       | massage_map _ _ t = raise NO_MAP t
     and massage_map_or_map_arg U T t =
       if T = U then
         tap check_no_call t
       else