# HG changeset patch
# User blanchet
# Date 1360916240 -3600
# Node ID fdcc06013f2db4737b8dba833a3601b444cb9eb3
# Parent  e32114b255511139431473aa696816a66132e054
avoid crude/wrong theorem comparision

diff -r e32114b25551 -r fdcc06013f2d src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Feb 15 09:17:20 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Fri Feb 15 09:17:20 2013 +0100
@@ -509,6 +509,10 @@
 val lams_feature = ("lams", 2.0 (* FUDGE *))
 val skos_feature = ("skos", 2.0 (* FUDGE *))
 
+(* The following "crude" functions should be progressively phased out, since
+   they create visibility edges that do not exist in Isabelle, resulting in
+   failed lookups later on. *)
+
 fun crude_theory_ord p =
   if Theory.subthy p then
     if Theory.eq_thy p then EQUAL else LESS
@@ -529,6 +533,9 @@
     end
   | ord => ord
 
+val thm_less_eq = Theory.subthy o pairself theory_of_thm
+fun thm_less p = thm_less_eq p andalso not (thm_less_eq (swap p))
+
 val freezeT = Type.legacy_freeze_type
 
 fun freeze (t $ u) = freeze t $ freeze u
@@ -696,8 +703,7 @@
       val thy = Proof_Context.theory_of ctxt
       val goal = goal_of_thm thy th
       val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
-      val facts =
-        facts |> filter (fn (_, th') => crude_thm_ord (th', th) = LESS)
+      val facts = facts |> filter (fn (_, th') => thm_less (th', th))
       fun nickify ((_, stature), th) = ((nickname_of_thm th, stature), th)
       fun is_dep dep (_, th) = nickname_of_thm th = dep
       fun add_isar_dep facts dep accum =