# HG changeset patch
# User blanchet
# Date 1626249763 -7200
# Node ID 2d8a0f8e30ec76fc6df426cf9f3def83592b2e21
# Parent  a5212df98387121b228efbeb91cd153d1032f6d2
correctly translate constructor argument in 'primrec'

diff -r a5212df98387 -r 2d8a0f8e30ec src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Tue Jul 13 15:25:53 2021 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Wed Jul 14 10:02:43 2021 +0200
@@ -366,7 +366,7 @@
               end)
         end
       | subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)
-      | subst _ t = t
+      | subst bound_Ts t = try_nested_rec bound_Ts (head_of t) t |> the_default t;
 
     fun subst' t =
       if has_call t then rec_call_not_apply_to_ctr_arg ctxt [] t