author blanchet Fri, 11 Jan 2013 16:30:56 +0100 changeset 50825 aed1d7242050 parent 50824 a991d603aac6 child 50826 18ace05656cf
always compare theorem using the same, weaker function
```--- 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
```--- 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