--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Feb 06 08:47:48 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Feb 06 19:17:17 2015 +0100
@@ -1116,10 +1116,12 @@
find_maxes Symtab.empty ([], Graph.maximals G)
end
+fun strict_subthy thyp = Theory.subthy thyp andalso not (Theory.subthy (swap thyp))
+
fun maximal_wrt_access_graph _ [] = []
| maximal_wrt_access_graph access_G ((fact as (_, th)) :: facts) =
let val thy = theory_of_thm th in
- fact :: filter_out (fn (_, th') => Theory.subthy (theory_of_thm th', thy)) facts
+ fact :: filter_out (fn (_, th') => strict_subthy (theory_of_thm th', thy)) facts
|> map (nickname_of_thm o snd)
|> maximal_wrt_graph access_G
end