added comment
authorblanchet
Wed May 21 14:09:43 2014 +0200 (2014-05-21)
changeset 570391ddd1f75fb40
parent 57038 2114f3224b2c
child 57040 fc96f394c7e5
added comment
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed May 21 14:09:42 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed May 21 14:09:43 2014 +0200
     1.3 @@ -806,6 +806,8 @@
     1.4  fun crude_thm_ord p =
     1.5    (case crude_theory_ord (pairself theory_of_thm p) of
     1.6      EQUAL =>
     1.7 +    (* The hack below is necessary because of odd dependencies that are not reflected in the theory
     1.8 +       comparison. *)
     1.9      let val q = pairself nickname_of_thm p in
    1.10        (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
    1.11        (case bool_ord (pairself (String.isSuffix "_def") (swap q)) of