extended the 'corec' format slightly

--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Wed Jul 14 16:09:57 2021 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Thu Jul 15 16:11:52 2021 +0200
@@ -983,10 +983,11 @@
     fun contains_res_T (Type (s, Ts)) = s = fst (dest_Type res_T) orelse exists contains_res_T Ts
       | contains_res_T _ = false;
 
-    val is_lhs_arg = member (op =) lhs_args;
+    val res_T_lhs_args = filter (exists_type contains_res_T) lhs_args;
+    val is_res_T_lhs_arg = member (op =) res_T_lhs_args;
 
     fun is_constant t =
-      not (Term.exists_subterm is_lhs_arg t orelse has_self_call t orelse loose_bvar (t, 0));
+      not (Term.exists_subterm is_res_T_lhs_arg t orelse has_self_call t orelse loose_bvar (t, 0));
     fun is_nested_type T = T <> res_T andalso T <> YpreT andalso T <> ssig_T;
 
     val is_valid_case_argumentT = not o member (op =) [Y, ssig_T];