# HG changeset patch
# User blanchet
# Date 1400674183 -7200
# Node ID 1ddd1f75fb404fb66fab19a8cace333dbd5ced45
# Parent  2114f3224b2cd17f46398796f9bac4d886507c2a
added comment

diff -r 2114f3224b2c -r 1ddd1f75fb40 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed May 21 14:09:42 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed May 21 14:09:43 2014 +0200
@@ -806,6 +806,8 @@
 fun crude_thm_ord p =
   (case crude_theory_ord (pairself theory_of_thm p) of
     EQUAL =>
+    (* The hack below is necessary because of odd dependencies that are not reflected in the theory
+       comparison. *)
     let val q = pairself nickname_of_thm p in
       (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
       (case bool_ord (pairself (String.isSuffix "_def") (swap q)) of