src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 50512 c283bc0a8f1a
parent 50511 8825c36cb1ce
child 50523 0799339fea0f
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 21:48:29 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Dec 12 21:48:29 2012 +0100
     1.3 @@ -183,7 +183,7 @@
     1.4    | apply_depth (Abs (_, _, t)) = apply_depth t
     1.5    | apply_depth _ = 0
     1.6  
     1.7 -fun is_formula_too_complex ho_atp t =
     1.8 +fun is_too_complex ho_atp t =
     1.9    apply_depth t > max_apply_depth orelse
    1.10    (not ho_atp andalso formula_has_too_many_lambdas [] t)
    1.11  
    1.12 @@ -236,7 +236,7 @@
    1.13  
    1.14  fun is_bad_for_atps ho_atp th =
    1.15    let val t = prop_of th in
    1.16 -    is_formula_too_complex ho_atp t orelse
    1.17 +    is_too_complex ho_atp t orelse
    1.18      exists_type type_has_top_sort t orelse exists_technical_const t orelse
    1.19      exists_low_level_class_const t orelse is_that_fact th
    1.20    end
    1.21 @@ -425,12 +425,12 @@
    1.22        Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
    1.23      fun add_facts global foldx facts =
    1.24        foldx (fn (name0, ths) =>
    1.25 -        if not really_all andalso
    1.26 -           name0 <> "" andalso
    1.27 +        if name0 <> "" andalso
    1.28             forall (not o member Thm.eq_thm_prop add_ths) ths andalso
    1.29             (Facts.is_concealed facts name0 orelse
    1.30              not (can (Proof_Context.get_thms ctxt) name0) orelse
    1.31 -            is_blacklisted_or_something ctxt ho_atp name0) then
    1.32 +            (not really_all andalso
    1.33 +             is_blacklisted_or_something ctxt ho_atp name0)) then
    1.34            I
    1.35          else
    1.36            let
    1.37 @@ -446,8 +446,7 @@
    1.38                     (j - 1,
    1.39                      if not (member Thm.eq_thm_prop add_ths th) andalso
    1.40                         is_likely_tautology_or_too_meta th orelse
    1.41 -                       (not really_all andalso
    1.42 -                        is_bad_for_atps ho_atp th) then
    1.43 +                       (not really_all andalso is_bad_for_atps ho_atp th) then
    1.44                        (multis, unis)
    1.45                      else
    1.46                        let