# HG changeset patch
# User blanchet
# Date 1307515663 -7200
# Node ID 956895f9990478018c2f4372be408f79714c6c02
# Parent  b81fd5c8f2dc38949713c72a29c87e65269bb986
slightly faster/cleaner accumulation of polymorphic consts

diff -r b81fd5c8f2dc -r 956895f99904 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 00:01:20 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jun 08 08:47:43 2011 +0200
@@ -368,10 +368,14 @@
    @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
    @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
 
-val atp_schematic_consts_of =
-  Monomorph.all_schematic_consts_of
-  #> Symtab.map (fn s => fn Ts =>
-                    if member (op =) atp_monomorph_bad_consts s then [] else Ts)
+fun add_schematic_const (x as (_, T)) =
+  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_monomorph_bad_consts s)
+                       ? add_schematic_const x
+                      | _ => I)
+fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
 
 (** Definitions and functions for FOL clauses and formulas for TPTP **)