# HG changeset patch
# User blanchet
# Date 1306188093 -7200
# Node ID c693f9b7674ae09c75938aa6f61a7e515d083d73
# Parent  9aeb0f6ad9710e7e5d6ff912e36ed6d6b5bfcc52
use "eq_thm_prop" for slacker comparison -- ensures that backtick-quoted chained facts are recognized in the minimizer, among other things

diff -r 9aeb0f6ad971 -r c693f9b7674a src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Tue May 24 00:01:33 2011 +0200
@@ -146,7 +146,7 @@
     (ths, (0, []))
     |-> fold (fn th => fn (j, rest) =>
                  (j + 1, ((nth_name j,
-                          if member Thm.eq_thm chained_ths th then Chained
+                          if member Thm.eq_thm_prop chained_ths th then Chained
                           else General), th) :: rest))
     |> snd
   end
@@ -600,7 +600,7 @@
               [Chained, Assum, Local]
     val add_ths = Attrib.eval_thms ctxt add
     val del_ths = Attrib.eval_thms ctxt del
-    val facts = facts |> filter_out (member Thm.eq_thm del_ths o snd)
+    val facts = facts |> filter_out (member Thm.eq_thm_prop del_ths o snd)
     fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
       let
         fun relevant [] _ [] =
@@ -673,12 +673,12 @@
           relevant [] [] hopeful
         end
     fun prepend_facts ths accepts =
-      ((facts |> filter (member Thm.eq_thm ths o snd)) @
-       (accepts |> filter_out (member Thm.eq_thm ths o snd)))
+      ((facts |> filter (member Thm.eq_thm_prop ths o snd)) @
+       (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)))
       |> take max_relevant
     fun append_facts ths accepts =
-      let val add = facts |> filter (member Thm.eq_thm ths o snd) in
-        (accepts |> filter_out (member Thm.eq_thm ths o snd)
+      let val add = facts |> filter (member Thm.eq_thm_prop ths o snd) in
+        (accepts |> filter_out (member Thm.eq_thm_prop ths o snd)
                  |> take (max_relevant - length add)) @
         add
       end
@@ -823,7 +823,7 @@
     val named_locals = local_facts |> Facts.dest_static []
     val assms = Assumption.all_assms_of ctxt
     fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms
-    val is_chained = member Thm.eq_thm chained_ths
+    val is_chained = member Thm.eq_thm_prop chained_ths
     val (intros, elims, simps) = clasimpset_rules_of ctxt
     fun locality_of_theorem global th =
       if is_chained th then
@@ -839,16 +839,16 @@
         if is_assum th then Assum else Local
     fun is_good_unnamed_local th =
       not (Thm.has_name_hint th) andalso
-      forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals
+      forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals
     val unnamed_locals =
-      union Thm.eq_thm (Facts.props local_facts) chained_ths
+      union Thm.eq_thm_prop (Facts.props local_facts) chained_ths
       |> filter is_good_unnamed_local |> map (pair "" o single)
     val full_space =
       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
-           forall (not o member Thm.eq_thm add_ths) ths andalso
+           forall (not o member Thm.eq_thm_prop add_ths) ths andalso
            (Facts.is_concealed facts name0 orelse
             (not (Config.get ctxt ignore_no_atp) andalso
              is_package_def name0) orelse
@@ -864,12 +864,12 @@
             fun check_thms a =
               case try (Proof_Context.get_thms ctxt) a of
                 NONE => false
-              | SOME ths' => Thm.eq_thms (ths, ths')
+              | SOME ths' => eq_list Thm.eq_thm_prop (ths, ths')
           in
             pair 1
             #> fold (fn th => fn (j, rest) =>
                         (j + 1,
-                         if not (member Thm.eq_thm add_ths th) andalso
+                         if not (member Thm.eq_thm_prop add_ths th) andalso
                             is_theorem_bad_for_atps is_appropriate_prop th then
                            rest
                          else