src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML

                    | NONE => subst_comb t))
                 | NONE => subst_comb t)
               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
       else try_nested_rec [] (head_of t) t |> the_default t;
   in