src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 50756 c96bb430ddb0
parent 50736 07dfdf72ab75
child 50815 41b804049fae
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun Jan 06 17:38:29 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun Jan 06 17:38:29 2013 +0100
     1.3 @@ -453,13 +453,13 @@
     1.4                | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
     1.5            in
     1.6              pair n
     1.7 -            #> fold_rev (fn th => fn (j, (multis, unis)) =>
     1.8 +            #> fold_rev (fn th => fn (j, accum) =>
     1.9                     (j - 1,
    1.10                      if not (member Thm.eq_thm_prop add_ths th) andalso
    1.11                         (is_likely_tautology_too_meta_or_too_technical th orelse
    1.12                          (not generous andalso
    1.13                           is_too_complex ho_atp (prop_of th))) then
    1.14 -                      (multis, unis)
    1.15 +                      accum
    1.16                      else
    1.17                        let
    1.18                          val new =
    1.19 @@ -469,23 +469,24 @@
    1.20                                  else
    1.21                                    [Facts.extern ctxt facts name0,
    1.22                                     Name_Space.extern ctxt full_space name0]
    1.23 +                                  |> distinct (op =)
    1.24                                    |> find_first check_thms
    1.25                                    |> the_default name0
    1.26                                    |> make_name reserved multi j),
    1.27                               stature_of_thm global assms chained css name0 th),
    1.28                             th)
    1.29                        in
    1.30 -                        if multi then (new :: multis, unis)
    1.31 -                        else (multis, new :: unis)
    1.32 +                        accum |> (if multi then apsnd else apfst) (cons new)
    1.33                        end)) ths
    1.34              #> snd
    1.35            end)
    1.36    in
    1.37 -    (* The single-name theorems go after the multiple-name ones, so that single
    1.38 -       names are preferred when both are available. *)
    1.39 -    ([], []) |> add_facts false fold local_facts (unnamed_locals @ named_locals)
    1.40 -             |> add_facts true Facts.fold_static global_facts global_facts
    1.41 -             |> op @
    1.42 +    (* The single-theorem names go before the multiple-theorem ones (e.g.,
    1.43 +       "xxx" vs. "xxx(3)"), so that single names are preferred when both are
    1.44 +       available. *)
    1.45 +    `I [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
    1.46 +          |> add_facts true Facts.fold_static global_facts global_facts
    1.47 +          |> op @
    1.48    end
    1.49  
    1.50  fun nearly_all_facts ctxt ho_atp {add, del, only} reserved css chained hyp_ts