# HG changeset patch
# User desharna
# Date 1639731162 -3600
# Node ID 90290869796f9e405aa6745d6089004c54efb1c6
# Parent  15ce207f69c8e7f3aaf5411bec41d0b092a1c3f5
tuned ATP to use is_widely_irrelevant_const

diff -r 15ce207f69c8 -r 90290869796f src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Dec 17 09:51:37 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Dec 17 09:52:42 2021 +0100
@@ -429,8 +429,7 @@
   Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
 val add_schematic_consts_of =
   Term.fold_aterms (fn Const (x as (s, _)) =>
-                       not (member (op =) atp_widely_irrelevant_consts s)
-                       ? add_schematic_const x
+                       not (is_widely_irrelevant_const s) ? add_schematic_const x
                       | _ => I)
 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty