src/HOL/Tools/ATP/atp_translate.ML
changeset 43258 956895f99904
parent 43248 69375eaa9016
child 43259 30c141dc22d6
--- 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 **)