1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Jun 07 14:17:35 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Jun 07 14:17:35 2011 +0200
     1.3 @@ -101,6 +101,8 @@
     1.4    val make_type_class : string -> string
     1.5    val new_skolem_var_name_from_const : string -> string
     1.6    val num_type_args : theory -> string -> int
     1.7 +  val atp_irrelevant_consts : string list
     1.8 +  val atp_schematic_consts_of : term -> typ list Symtab.table
     1.9    val make_arity_clauses :
    1.10      theory -> string list -> class list -> class list * arity_clause list
    1.11    val make_class_rel_clauses :
    1.12 @@ -351,6 +353,26 @@
    1.13    else
    1.14      (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
    1.15  
    1.16 +(* These are either simplified away by "Meson.presimplify" (most of the time) or
    1.17 +   handled specially via "fFalse", "fTrue", ..., "fequal". *)
    1.18 +val atp_irrelevant_consts =
    1.19 +  [@{const_name False}, @{const_name True}, @{const_name Not},
    1.20 +   @{const_name conj}, @{const_name disj}, @{const_name implies},
    1.21 +   @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
    1.22 +
    1.23 +val atp_monomorph_bad_consts =
    1.24 +  atp_irrelevant_consts @
    1.25 +  (* These are ignored anyway by the relevance filter (unless they appear in
    1.26 +     higher-order places) but not by the monomorphizer. *)
    1.27 +  [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
    1.28 +   @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
    1.29 +   @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
    1.30 +
    1.31 +val atp_schematic_consts_of =
    1.32 +  Monomorph.all_schematic_consts_of
    1.33 +  #> Symtab.map (fn s => fn Ts =>
    1.34 +                    if member (op =) atp_monomorph_bad_consts s then [] else Ts)
    1.35 +
    1.36  (** Definitions and functions for FOL clauses and formulas for TPTP **)
    1.37  
    1.38  (* The first component is the type class; the second is a "TVar" or "TFree". *)