src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
changeset 57039 1ddd1f75fb40
parent 57029 75cc30d2b83f
child 57052 ea5912e3b008
     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