--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 18 08:44:04 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 18 08:44:04 2012 +0200
@@ -85,8 +85,8 @@
val invert_const : string -> string
val unproxify_const : string -> string
val new_skolem_var_name_from_const : string -> string
+ val atp_logical_consts : string list
val atp_irrelevant_consts : string list
- val atp_widely_irrelevant_consts : string list
val atp_schematic_consts_of : term -> typ list Symtab.table
val is_type_enc_higher_order : type_enc -> bool
val is_type_enc_polymorphic : type_enc -> bool
@@ -390,6 +390,13 @@
nth ss (length ss - 2)
end
+(* These are ignored anyway by the relevance filter (unless they appear in
+ higher-order places) but not by the monomorphizer. *)
+val atp_logical_consts =
+ [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
+ @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
+ @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
+
(* These are either simplified away by "Meson.presimplify" (most of the time) or
handled specially via "fFalse", "fTrue", ..., "fequal". *)
val atp_irrelevant_consts =
@@ -397,13 +404,7 @@
@{const_name conj}, @{const_name disj}, @{const_name implies},
@{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
-val atp_widely_irrelevant_consts =
- atp_irrelevant_consts @
- (* These are ignored anyway by the relevance filter (unless they appear in
- higher-order places) but not by the monomorphizer. *)
- [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
- @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
- @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
+val atp_widely_irrelevant_consts = atp_logical_consts @ atp_irrelevant_consts
fun add_schematic_const (x as (_, T)) =
Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x