# HG changeset patch
# User Mathias Fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1656131651 -7200
# Node ID 66edc020a3220f25affe09fce4516a8028e233c1
# Parent  da901dcafc2952be3709c60f102b1567c3f28daf
missing recursive let-expansion in SMT translation

diff -r da901dcafc29 -r 66edc020a322 src/HOL/Tools/SMT/smt_translate.ML
--- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Jun 24 21:17:35 2022 +0200
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Sat Jun 25 06:34:11 2022 +0200
@@ -210,7 +210,7 @@
       | expand (q as Const (\<^const_name>\<open>Ex\<close>, T)) = exp2 T q
       | expand (Const (\<^const_name>\<open>Let\<close>, T) $ t) =
           let val U = Term.domain_type (Term.range_type T)
-          in Abs (Name.uu, U, Bound 0 $ Term.incr_boundvars 1 t) end
+          in Abs (Name.uu, U, expand (Bound 0 $ Term.incr_boundvars 1 t)) end
       | expand (Const (\<^const_name>\<open>Let\<close>, T)) =
           let val U = Term.domain_type (Term.range_type T)
           in Abs (Name.uu, Term.domain_type T, Abs (Name.uu, U, Bound 0 $ Bound 1)) end