further optimization in relevance filter
authorblanchet
Tue Oct 08 16:40:03 2013 +0200 (2013-10-08 ago)
changeset 540781d371c3f2703
parent 54077 af65902b6e30
child 54079 cb33b304e743
further optimization in relevance filter
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 08 14:53:33 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 08 16:40:03 2013 +0200
     1.3 @@ -378,9 +378,12 @@
     1.4      val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
     1.5    in (plain_name_tab, inclass_name_tab) end
     1.6  
     1.7 +(* The function would have slightly cleaner semantics if it called "Pattern.equiv" instead of
     1.8 +   "Pattern.matches", but it would also be slower. "Pattern.matches" throws out theorems that are
     1.9 +   strict instances of other theorems, but only if the instance is met after the general version. *)
    1.10  fun fact_distinct thy facts =
    1.11    fold (fn fact as (_, th) =>
    1.12 -      Net.insert_term_safe (Pattern.equiv thy o pairself (normalize_eq o prop_of o snd))
    1.13 +      Net.insert_term_safe (Pattern.matches thy o swap o pairself (normalize_eq o prop_of o snd))
    1.14          (normalize_eq (prop_of th), fact))
    1.15      facts Net.empty
    1.16    |> Net.entries