# HG changeset patch
# User blanchet
# Date 1355345309 -3600
# Node ID c283bc0a8f1aaee0aa20a309347d78bd8cf4d829
# Parent  8825c36cb1cebcfe4e08708fccac3229bc5c8a46
tweaked which facts are included for MaSh evaluations

diff -r 8825c36cb1ce -r c283bc0a8f1a src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 21:48:29 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 21:48:29 2012 +0100
@@ -183,7 +183,7 @@
   | apply_depth (Abs (_, _, t)) = apply_depth t
   | apply_depth _ = 0
 
-fun is_formula_too_complex ho_atp t =
+fun is_too_complex ho_atp t =
   apply_depth t > max_apply_depth orelse
   (not ho_atp andalso formula_has_too_many_lambdas [] t)
 
@@ -236,7 +236,7 @@
 
 fun is_bad_for_atps ho_atp th =
   let val t = prop_of th in
-    is_formula_too_complex ho_atp t orelse
+    is_too_complex ho_atp t orelse
     exists_type type_has_top_sort t orelse exists_technical_const t orelse
     exists_low_level_class_const t orelse is_that_fact th
   end
@@ -425,12 +425,12 @@
       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 name0 <> "" andalso
            forall (not o member Thm.eq_thm_prop add_ths) ths andalso
            (Facts.is_concealed facts name0 orelse
             not (can (Proof_Context.get_thms ctxt) name0) orelse
-            is_blacklisted_or_something ctxt ho_atp name0) then
+            (not really_all andalso
+             is_blacklisted_or_something ctxt ho_atp name0)) then
           I
         else
           let
@@ -446,8 +446,7 @@
                    (j - 1,
                     if not (member Thm.eq_thm_prop add_ths th) andalso
                        is_likely_tautology_or_too_meta th orelse
-                       (not really_all andalso
-                        is_bad_for_atps ho_atp th) then
+                       (not really_all andalso is_bad_for_atps ho_atp th) then
                       (multis, unis)
                     else
                       let