# HG changeset patch
# User blanchet
# Date 1309179393 -7200
# Node ID ebeda6275027a67dd9b072dcbfaf5560a4a6fe60
# Parent  cfb2077cb2dba62db351eed3de6013dff8cc2975
don't export any metastrange or other nonatomizable formulas, since these don't help proving normal things, they are somewhat broken in the ATP output, and they are atypical

diff -r cfb2077cb2db -r ebeda6275027 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Jun 27 14:56:32 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Jun 27 14:56:33 2011 +0200
@@ -776,9 +776,9 @@
 
 fun is_metastrange_theorem th =
   case head_of (concl_of th) of
-      Const (a, _) => (a <> @{const_name Trueprop} andalso
-                       a <> @{const_name "=="})
-    | _ => false
+    Const (s, _) => (s <> @{const_name Trueprop} andalso
+                     s <> @{const_name "=="})
+  | _ => false
 
 fun is_that_fact th =
   String.isSuffix (Long_Name.separator ^ Obtain.thatN) (Thm.get_name_hint th)
@@ -791,12 +791,14 @@
 (**** Predicates to detect unwanted facts (prolific or likely to cause
       unsoundness) ****)
 
-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
-    exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
-    is_metastrange_theorem thm orelse is_that_fact thm
-  end
+fun is_theorem_bad_for_atps exporter thm =
+  is_metastrange_theorem thm orelse
+  (not exporter andalso
+   let val t = prop_of thm in
+     is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
+     exists_sledgehammer_const t orelse exists_low_level_class_const t orelse
+     is_that_fact thm
+   end)
 
 fun meta_equify (@{const Trueprop}
                  $ (Const (@{const_name HOL.eq}, Type (_, [T, _])) $ t1 $ t2)) =
@@ -822,7 +824,7 @@
                   |> add Simp normalize_simp_prop snd simps
   end
 
-fun all_facts ctxt reserved really_all add_ths chained_ths =
+fun all_facts ctxt reserved exporter add_ths chained_ths =
   let
     val thy = Proof_Context.theory_of ctxt
     val global_facts = Global_Theory.facts_of thy
@@ -852,7 +854,7 @@
       Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
     fun add_facts global foldx facts =
       foldx (fn (name0, ths) =>
-        if not really_all andalso name0 <> "" andalso
+        if not exporter andalso name0 <> "" andalso
            forall (not o member Thm.eq_thm_prop add_ths) ths andalso
            (Facts.is_concealed facts name0 orelse
             (not (Config.get ctxt ignore_no_atp) andalso
@@ -874,9 +876,8 @@
             pair 1
             #> fold (fn th => fn (j, (multis, unis)) =>
                         (j + 1,
-                         if not really_all andalso
-                            not (member Thm.eq_thm_prop add_ths th) andalso
-                            is_theorem_bad_for_atps th then
+                         if not (member Thm.eq_thm_prop add_ths th) andalso
+                            is_theorem_bad_for_atps exporter th then
                            (multis, unis)
                          else
                            let
diff -r cfb2077cb2db -r ebeda6275027 src/HOL/ex/atp_export.ML
--- a/src/HOL/ex/atp_export.ML	Mon Jun 27 14:56:32 2011 +0200
+++ b/src/HOL/ex/atp_export.ML	Mon Jun 27 14:56:33 2011 +0200
@@ -29,6 +29,8 @@
 fun facts_of thy =
   Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) Symtab.empty
                                 true [] []
+  |> filter (curry (op =) @{typ bool} o fastype_of
+             o Object_Logic.atomize_term thy o prop_of o snd)
 
 (* FIXME: Similar yet different code in "mirabelle.ML". The code here has a few
    fixes that seem to be missing over there; or maybe the two code portions are
@@ -153,22 +155,20 @@
     val type_sys = type_sys |> type_sys_from_string
     val path = file_name |> Path.explode
     val _ = File.write path ""
-    val facts0 = facts_of thy
-    val facts =
-      facts0 |> map (fn ((_, loc), th) =>
-                        ((Thm.get_name_hint th, loc), prop_of th))
+    val facts = facts_of thy
     val (atp_problem, _, _, _, _, _, _) =
-      prepare_atp_problem ctxt format Axiom Axiom type_sys true true false true
-                          [] @{prop False} facts
+      facts
+      |> map (fn ((_, loc), th) => ((Thm.get_name_hint th, loc), prop_of th))
+      |> prepare_atp_problem ctxt format Axiom Axiom type_sys true true false
+                             true [] @{prop False}
     val atp_problem =
       atp_problem
       |> map (apsnd (filter_out (is_problem_line_tautology ctxt)))
-    val all_names = facts0 |> map (Thm.get_name_hint o snd)
+    val all_names = facts |> map (Thm.get_name_hint o snd)
     val infers =
-      facts0 |> map (fn (_, th) =>
-                        (fact_name_of (Thm.get_name_hint th),
-                         theorems_mentioned_in_proof_term (SOME all_names) th))
-
+      facts |> map (fn (_, th) =>
+                       (fact_name_of (Thm.get_name_hint th),
+                        theorems_mentioned_in_proof_term (SOME all_names) th))
     val all_atp_problem_names =
       atp_problem |> maps (map ident_of_problem_line o snd)
     val infers =