# HG changeset patch
# User desharna
# Date 1635932694 -3600
# Node ID d4a812e4f041f89d76e3c052af0984d90a50cf82
# Parent  d4ef127b74df85dc9f7cd39763c564670b518bb9# Parent  591303cc04c2e3f93a14122bd8611c9ab53d1ba2
merged

diff -r 591303cc04c2 -r d4a812e4f041 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Nov 03 00:42:05 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Nov 03 10:44:54 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)) =
diff -r 591303cc04c2 -r d4a812e4f041 src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Wed Nov 03 00:42:05 2021 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Wed Nov 03 10:44:54 2021 +0100
@@ -940,8 +940,8 @@
            (map_id0N, [#map_id0 axioms], []),
            (map_transferN, [Lazy.force (#map_transfer facts)], []),
            (map_identN, [Lazy.force (#map_ident facts)], []),
+           (pred_monoN, [Lazy.force (#pred_mono facts)], mono_attrs),
            (pred_mono_strongN, [Lazy.force (#pred_mono_strong facts)], []),
-           (pred_monoN, [Lazy.force (#pred_mono facts)], []),
            (pred_congN, [Lazy.force (#pred_cong facts)], fundefcong_attrs),
            (pred_cong_simpN, [Lazy.force (#pred_cong_simp facts)], []),
            (pred_mapN, [Lazy.force (#pred_map facts)], []),