# HG changeset patch
# User blanchet
# Date 1381243203 -7200
# Node ID 1d371c3f2703520997278de7d1ca6dfcb0929c8c
# Parent  af65902b6e309b01f739485ba764eeb07e351b35
further optimization in relevance filter

diff -r af65902b6e30 -r 1d371c3f2703 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 08 14:53:33 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Oct 08 16:40:03 2013 +0200
@@ -378,9 +378,12 @@
     val inclass_name_tab = Symtab.fold add_inclass plain_name_tab Symtab.empty
   in (plain_name_tab, inclass_name_tab) end
 
+(* The function would have slightly cleaner semantics if it called "Pattern.equiv" instead of
+   "Pattern.matches", but it would also be slower. "Pattern.matches" throws out theorems that are
+   strict instances of other theorems, but only if the instance is met after the general version. *)
 fun fact_distinct thy facts =
   fold (fn fact as (_, th) =>
-      Net.insert_term_safe (Pattern.equiv thy o pairself (normalize_eq o prop_of o snd))
+      Net.insert_term_safe (Pattern.matches thy o swap o pairself (normalize_eq o prop_of o snd))
         (normalize_eq (prop_of th), fact))
     facts Net.empty
   |> Net.entries