careful about visibility of facts that have the same 'theory' in optimization

--- 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