# HG changeset patch
# User desharna
# Date 1635838208 -3600
# Node ID b74dfca75e84065d24f111bd73f31925fe661c57
# Parent  cd674ebf6cac34bc8ba4c877433097bd01aabb25# Parent  44585660f39aeb0b9d4f2ddf5787cee116b66833
merged

diff -r cd674ebf6cac -r b74dfca75e84 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Nov 01 23:13:14 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Nov 02 08:30:08 2021 +0100
@@ -2312,7 +2312,9 @@
                 SOME ({pred_sym, in_conj, ...} : sym_info) => (pred_sym, in_conj)
               | NONE => (false, false))
             val decl_sym =
-              (case type_enc of Guards _ => not pred_sym | _ => true) andalso is_tptp_user_symbol s
+              (case type_enc of Guards _ => not pred_sym | _ => true) andalso
+              not (String.isPrefix let_bound_var_prefix s) andalso
+              is_tptp_user_symbol s
           in
             if decl_sym then
               Symtab.map_default (s, [])
@@ -2724,7 +2726,10 @@
 fun undeclared_in_problem problem =
   let
     fun do_sym (name as (s, _)) value =
-      if is_tptp_user_symbol s then Symtab.default (s, (name, value)) else I
+      if is_tptp_user_symbol s andalso not (String.isPrefix let_bound_var_prefix s) then
+        Symtab.default (s, (name, value))
+      else
+        I
     fun do_class name = apfst (apfst (do_sym name ()))
     val do_bound_tvars = fold do_class o snd
     fun do_type (AType ((name, _), tys)) =