# HG changeset patch
# User blanchet
# Date 1357918256 -3600
# Node ID aed1d72420507179eaafbf1b94189401c20c54d5
# Parent  a991d603aac6deaacdfac4165bfe3e1a38250cc2
always compare theorem using the same, weaker function

diff -r a991d603aac6 -r aed1d7242050 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Fri Jan 11 14:35:28 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Fri Jan 11 16:30:56 2013 +0100
@@ -91,7 +91,7 @@
             [(mepo_weight, (mepo_facts, [])),
              (mash_weight, (mash_facts, mash_unks))]
           val mesh_facts =
-            mesh_facts (Thm.eq_thm o pairself snd) slack_max_facts mess
+            mesh_facts (Thm.eq_thm_prop o pairself snd) slack_max_facts mess
           val isar_facts =
             find_suggested_facts (map (rpair 1.0) isar_deps) facts
           (* adapted from "mirabelle_sledgehammer.ML" *)
diff -r a991d603aac6 -r aed1d7242050 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 11 14:35:28 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Jan 11 16:30:56 2013 +0100
@@ -771,7 +771,7 @@
     val unknown =
       raw_unknown
       |> fold (subtract (Thm.eq_thm_prop o pairself snd)) [chained, proximity]
-  in (mesh_facts (Thm.eq_thm o pairself snd) max_facts mess, unknown) end
+  in (mesh_facts (Thm.eq_thm_prop o pairself snd) max_facts mess, unknown) end
 
 fun mash_suggested_facts ctxt ({overlord, ...} : params) prover max_facts hyp_ts
                          concl_t facts =
@@ -1116,7 +1116,7 @@
            |> (if fact_filter <> mepoN then cons (mash_weight, (mash ()))
                else I)
     in
-      mesh_facts (Thm.eq_thm o pairself snd) max_facts mess
+      mesh_facts (Thm.eq_thm_prop o pairself snd) max_facts mess
       |> not (null add_ths) ? prepend_facts add_ths
     end