have each ATP filter out dangerous facts for themselves, based on their type system

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon May 02 22:31:46 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon May 02 22:52:15 2011 +0200
@@ -377,8 +377,6 @@
       Sledgehammer_Provers.relevance_fudge_for_prover ctxt prover_name
     val relevance_override = {add = [], del = [], only = false}
     val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
-    val fairly_sound =
-      Sledgehammer_Provers.is_rich_type_sys_fairly_sound type_sys
     val time_limit =
       (case hard_timeout of
         NONE => I
@@ -388,8 +386,7 @@
         time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
       let
         val facts =
-          Sledgehammer_Filter.relevant_facts ctxt fairly_sound
-              relevance_thresholds
+          Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
               (the_default default_max_relevant max_relevant) is_built_in_const
               relevance_fudge relevance_override chained_ths hyp_ts concl_t
         val problem =

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon May 02 22:31:46 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Mon May 02 22:52:15 2011 +0200
@@ -125,11 +125,8 @@
          val relevance_override = {add = [], del = [], only = false}
          val subgoal = 1
          val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
-         val fairly_sound =
-           Sledgehammer_Provers.is_rich_type_sys_fairly_sound type_sys
          val facts =
-           Sledgehammer_Filter.relevant_facts ctxt fairly_sound
-               relevance_thresholds
+           Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
                (the_default default_max_relevant max_relevant) is_built_in_const
                relevance_fudge relevance_override facts hyp_ts concl_t
            |> map (fst o fst)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon May 02 22:31:46 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon May 02 22:52:15 2011 +0200
@@ -41,13 +41,14 @@
     Proof.context -> unit Symtab.table -> thm list
     -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list
   val all_facts :
-    Proof.context -> 'a Symtab.table -> bool -> bool -> relevance_fudge
-    -> thm list -> thm list -> (((unit -> string) * locality) * (bool * thm)) list
+    Proof.context -> 'a Symtab.table -> bool -> relevance_fudge -> thm list
+    -> thm list -> (((unit -> string) * locality) * (bool * thm)) list
   val const_names_in_fact :
     theory -> (string * typ -> term list -> bool * term list) -> term
     -> string list
+  val is_dangerous_term : term -> bool
   val relevant_facts :
-    Proof.context -> bool -> real * real -> int
+    Proof.context -> real * real -> int
     -> (string * typ -> term list -> bool * term list) -> relevance_fudge
     -> relevance_override -> thm list -> term list -> term
     -> ((string * locality) * thm) list
@@ -772,24 +773,20 @@
    equations like "?x = ()". The resulting clauses will have no type constraint,
    yielding false proofs. Even "bool" leads to many unsound proofs, though only
    for higher-order problems. *)
-val dangerous_types = [@{type_name unit}, @{type_name bool}, @{type_name prop}];
+val dangerous_types = [@{type_name unit}, @{type_name bool}, @{type_name prop}]
 
 (* Facts containing variables of type "unit" or "bool" or of the form
    "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
    are omitted. *)
-fun is_dangerous_term fairly_sound t =
-  not fairly_sound andalso
-  let val t = transform_elim_term t in
-    has_bound_or_var_of_type dangerous_types t orelse
-    is_exhaustive_finite t
-  end
+val is_dangerous_term =
+  transform_elim_term
+  #> has_bound_or_var_of_type dangerous_types orf is_exhaustive_finite
 
-fun is_theorem_bad_for_atps fairly_sound thm =
+fun is_theorem_bad_for_atps thm =
   let val t = prop_of thm in
     is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
-    is_dangerous_term fairly_sound t orelse exists_sledgehammer_const t orelse
-    exists_low_level_class_const t orelse is_metastrange_theorem thm orelse
-    is_that_fact thm
+    exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
+    is_metastrange_theorem thm orelse is_that_fact thm
   end
 
 fun clasimpset_rules_of ctxt =
@@ -800,7 +797,7 @@
     val simps = ctxt |> simpset_of |> dest_ss |> #simps |> map snd
   in (mk_fact_table I intros, mk_fact_table I elims, mk_fact_table I simps) end
 
-fun all_facts ctxt reserved really_all fairly_sound
+fun all_facts ctxt reserved really_all
               ({intro_bonus, elim_bonus, simp_bonus, ...} : relevance_fudge)
               add_ths chained_ths =
   let
@@ -846,7 +843,7 @@
             pair 1
             #> fold (fn th => fn (j, rest) =>
                  (j + 1,
-                  if is_theorem_bad_for_atps fairly_sound th andalso
+                  if is_theorem_bad_for_atps th andalso
                      not (member Thm.eq_thm add_ths th) then
                     rest
                   else
@@ -890,9 +887,9 @@
 fun external_frees t =
   [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
 
-fun relevant_facts ctxt fairly_sound (threshold0, threshold1) max_relevant
-                   is_built_in_const fudge (override as {add, only, ...})
-                   chained_ths hyp_ts concl_t =
+fun relevant_facts ctxt (threshold0, threshold1) max_relevant is_built_in_const
+                   fudge (override as {add, only, ...}) chained_ths hyp_ts
+                   concl_t =
   let
     val thy = Proof_Context.theory_of ctxt
     val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
@@ -908,7 +905,7 @@
          maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
                o fact_from_ref ctxt reserved chained_ths) add
        else
-         all_facts ctxt reserved false fairly_sound fudge add_ths chained_ths)
+         all_facts ctxt reserved false fudge add_ths chained_ths)
       |> instantiate_inducts
          ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
       |> rearrange_facts ctxt (respect_no_atp andalso not only)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 02 22:31:46 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Mon May 02 22:52:15 2011 +0200
@@ -68,7 +68,7 @@
   val smt_slice_fact_frac : real Unsynchronized.ref
   val smt_slice_time_frac : real Unsynchronized.ref
   val smt_slice_min_secs : int Unsynchronized.ref
-
+  (* end *)
   val das_Tool : string
   val select_smt_solver : string -> Proof.context -> Proof.context
   val is_smt_prover : Proof.context -> string -> bool
@@ -86,7 +86,6 @@
   val weight_smt_fact :
     theory -> int -> ((string * locality) * thm) * int
     -> (string * locality) * (int option * thm)
-  val is_rich_type_sys_fairly_sound : rich_type_system -> bool
   val untranslated_fact : prover_fact -> (string * locality) * thm
   val smt_weighted_fact :
     theory -> int -> prover_fact * int
@@ -312,10 +311,6 @@
 fun weight_smt_fact thy num_facts ((info, th), j) =
   (info, (smt_fact_weight j num_facts, th |> Thm.transfer thy))
 
-fun is_rich_type_sys_fairly_sound (Dumb_Type_Sys type_sys) =
-    is_type_sys_fairly_sound type_sys
-  | is_rich_type_sys_fairly_sound (Smart_Type_Sys full_types) = full_types
-
 fun untranslated_fact (Untranslated_Fact p) = p
   | untranslated_fact (SMT_Weighted_Fact (info, (_, th))) = (info, th)
 fun atp_translated_fact ctxt fact =
@@ -432,8 +427,12 @@
                 val num_facts =
                   length facts |> is_none max_relevant
                                   ? Integer.min default_max_relevant
+                val fairly_sound = is_type_sys_fairly_sound type_sys
                 val facts =
-                  facts |> take num_facts
+                  facts |> fairly_sound
+                           ? filter_out (is_dangerous_term o prop_of o snd
+                                         o untranslated_fact)
+                        |> take num_facts
                         |> not (null blacklist)
                            ? filter_out (member (op =) blacklist o fst
                                          o untranslated_fact)
@@ -718,7 +717,7 @@
                 " fact" ^ plural_s num_facts ^ ": " ^
                 string_for_failure (failure_from_smt_failure (the outcome)) ^
                 " Retrying with " ^ string_of_int new_num_facts ^ " fact" ^
-                plural_s new_num_facts
+                plural_s new_num_facts ^ "..."
                 |> Output.urgent_message
               else
                 ()

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon May 02 22:31:46 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon May 02 22:52:15 2011 +0200
@@ -99,7 +99,7 @@
       prover_description ctxt params name num_facts subgoal subgoal_count goal
     val problem =
       {state = state, goal = goal, subgoal = subgoal,
-       subgoal_count = subgoal_count, facts = take num_facts facts,
+       subgoal_count = subgoal_count, facts = facts |> take num_facts,
        smt_filter = smt_filter}
     fun really_go () =
       problem
@@ -182,7 +182,6 @@
       val thy = Proof_Context.theory_of ctxt
       val {facts = chained_ths, goal, ...} = Proof.goal state
       val (_, hyp_ts, concl_t) = strip_subgoal goal i
-      val fairly_sound = is_rich_type_sys_fairly_sound type_sys
       val _ = () |> not blocking ? kill_provers
       val _ = case find_first (not o is_prover_supported ctxt) provers of
                 SOME name => error ("No such prover: " ^ name ^ ".")
@@ -211,7 +210,7 @@
             |> (if blocking then smart_par_list_map else map) (launch problem)
             |> exists fst |> rpair state
         end
-      fun get_facts label fairly_sound relevance_fudge provers =
+      fun get_facts label relevance_fudge provers =
         let
           val max_max_relevant =
             case max_relevant of
@@ -224,7 +223,7 @@
           val is_built_in_const =
             is_built_in_const_for_prover ctxt (hd provers)
         in
-          relevant_facts ctxt fairly_sound relevance_thresholds max_max_relevant
+          relevant_facts ctxt relevance_thresholds max_max_relevant
                          is_built_in_const relevance_fudge relevance_override
                          chained_ths hyp_ts concl_t
           |> tap (fn facts =>
@@ -244,15 +243,14 @@
         if null atps then
           accum
         else
-          launch_provers state
-              (get_facts "ATP" fairly_sound atp_relevance_fudge o K atps)
-              (K (Untranslated_Fact o fst)) (K (K NONE)) atps
+          launch_provers state (get_facts "ATP" atp_relevance_fudge o K atps)
+                         (K (Untranslated_Fact o fst)) (K (K NONE)) atps
       fun launch_smts accum =
         if null smts then
           accum
         else
           let
-            val facts = get_facts "SMT solver" true smt_relevance_fudge smts
+            val facts = get_facts "SMT solver" smt_relevance_fudge smts
             val weight = SMT_Weighted_Fact oo weight_smt_fact thy
             fun smt_filter facts =
               (if debug then curry (op o) SOME

--- a/src/HOL/ex/sledgehammer_tactics.ML	Mon May 02 22:31:46 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML	Mon May 02 22:52:15 2011 +0200
@@ -32,10 +32,8 @@
       Sledgehammer_Provers.relevance_fudge_for_prover ctxt name
     val relevance_override = {add = [], del = [], only = false}
     val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal i
-    val fairly_sound =
-      Sledgehammer_Provers.is_rich_type_sys_fairly_sound type_sys
     val facts =
-      Sledgehammer_Filter.relevant_facts ctxt fairly_sound relevance_thresholds
+      Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
           (the_default default_max_relevant max_relevant) is_built_in_const
           relevance_fudge relevance_override chained_ths hyp_ts concl_t
     val problem =

--- a/src/HOL/ex/tptp_export.ML	Mon May 02 22:31:46 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML	Mon May 02 22:52:15 2011 +0200
@@ -22,7 +22,7 @@
 val fact_name_of = prefix Sledgehammer_ATP_Translate.fact_prefix o ascii_of
 
 fun facts_of thy =
-  Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty true
+  Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty
       true Sledgehammer_Provers.atp_relevance_fudge [] []
 
 fun fold_body_thms f =