proper treatment of $let variables in symbol table in Sledgehammer
authordesharna
Sun, 16 Jan 2022 21:41:16 +0100
changeset 74984 192876ea202d
parent 74983 b87fcf474e7f
child 74985 ac3901e4e0a9
proper treatment of $let variables in symbol table in Sledgehammer
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