# HG changeset patch
# User blanchet
# Date 1626358312 -7200
# Node ID 84528a343f5f8afbf287076601de109705cd9bc9
# Parent  291f7b5fc7c9cbfca6c3516f2636eb1df60950fa
extended the 'corec' format slightly

diff -r 291f7b5fc7c9 -r 84528a343f5f src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- 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];