# HG changeset patch
# User blanchet
# Date 1423246637 -3600
# Node ID 2025a17bb20fa59c9f86a9ec22f8794526cec2f7
# Parent  792272e6ee6b0204f72329300f38fe4e8b9a621a
careful about visibility of facts that have the same 'theory' in optimization

diff -r 792272e6ee6b -r 2025a17bb20f src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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