correctly translate constructor argument in 'primrec'

--- 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