# HG changeset patch
# User desharna
# Date 1642365676 -3600
# Node ID 192876ea202d693c268306efa5e50894f65568bc
# Parent  b87fcf474e7f19254e21b09a0e63c7dec7cc3c93
proper treatment of $let variables in symbol table in Sledgehammer

diff -r b87fcf474e7f -r 192876ea202d src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Jan 15 14:26:16 2022 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Jan 16 21:41:16 2022 +0100
@@ -1643,7 +1643,7 @@
       let val (head, args) = strip_iterm_comb tm in
         (case head of
           IConst ((s, _), T, _) =>
-          if is_maybe_universal_name s then
+          if is_maybe_universal_name s orelse String.isPrefix let_bound_var_prefix s then
             add_universal_var T accum
           else if String.isPrefix exist_bound_var_prefix s then
             accum