Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
changeset 73977 2d8a0f8e30ec
parent 71214 5727bcc3c47c
child 74561 8e6c973003c8 
--- 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
isabelle