# HG changeset patch
# User blanchet
# Date 1307449055 -7200
# Node ID 69375eaa90165f94b571f61a3bd057bef0e36b36
# Parent  4387af606a09e2d9ffc95cb58f523ef7c373a457
more suitable implementation of "schematic_consts_of" for monomorphizer, for ATPs

diff -r 4387af606a09 -r 69375eaa9016 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Jun 07 14:17:35 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Jun 07 14:17:35 2011 +0200
@@ -101,6 +101,8 @@
   val make_type_class : string -> string
   val new_skolem_var_name_from_const : string -> string
   val num_type_args : theory -> string -> int
+  val atp_irrelevant_consts : string list
+  val atp_schematic_consts_of : term -> typ list Symtab.table
   val make_arity_clauses :
     theory -> string list -> class list -> class list * arity_clause list
   val make_class_rel_clauses :
@@ -351,6 +353,26 @@
   else
     (s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
 
+(* These are either simplified away by "Meson.presimplify" (most of the time) or
+   handled specially via "fFalse", "fTrue", ..., "fequal". *)
+val atp_irrelevant_consts =
+  [@{const_name False}, @{const_name True}, @{const_name Not},
+   @{const_name conj}, @{const_name disj}, @{const_name implies},
+   @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
+
+val atp_monomorph_bad_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_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)
+
 (** Definitions and functions for FOL clauses and formulas for TPTP **)
 
 (* The first component is the type class; the second is a "TVar" or "TFree". *)
diff -r 4387af606a09 -r 69375eaa9016 src/HOL/Tools/Metis/metis_translate.ML
--- a/src/HOL/Tools/Metis/metis_translate.ML	Tue Jun 07 14:17:35 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML	Tue Jun 07 14:17:35 2011 +0200
@@ -175,7 +175,7 @@
           else
             map (pair 0)
             #> rpair ctxt
-            #-> Monomorph.monomorph Monomorph.all_schematic_consts_of
+            #-> Monomorph.monomorph atp_schematic_consts_of
             #> fst #> maps (map (zero_var_indexes o snd)))
     val (old_skolems, props) =
       fold_rev (fn clause => fn (old_skolems, props) =>
diff -r 4387af606a09 -r 69375eaa9016 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 14:17:35 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Jun 07 14:17:35 2011 +0200
@@ -184,13 +184,6 @@
       SMT_Solver.default_max_relevant ctxt name
   end
 
-(* These are either simplified away by "Meson.presimplify" (most of the time) or
-   handled specially via "fFalse", "fTrue", ..., "fequal". *)
-val atp_irrelevant_consts =
-  [@{const_name False}, @{const_name True}, @{const_name Not},
-   @{const_name conj}, @{const_name disj}, @{const_name implies},
-   @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
-
 fun is_if (@{const_name If}, _) = true
   | is_if _ = false
 
@@ -611,7 +604,7 @@
                   Logic.list_implies (hyp_ts, concl_t)
                   |> Skip_Proof.make_thm thy
               in
-                Monomorph.monomorph Monomorph.all_schematic_consts_of
+                Monomorph.monomorph atp_schematic_consts_of
                     (subgoal_th :: map snd facts |> map (pair 0)) ctxt
                 |> fst |> tl
                 |> curry ListPair.zip (map fst facts)