--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Dec 04 23:50:36 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Wed Dec 05 10:35:58 2012 +0100
@@ -473,7 +473,12 @@
EQUAL => string_ord (pairself Context.theory_name p)
| order => order
-val thm_ord = theory_ord o pairself theory_of_thm
+fun thm_ord thp =
+ case theory_ord (pairself theory_of_thm thp) of
+ EQUAL =>
+ (* Hack to put "xxx_def" before "xxxI" and "xxxE" *)
+ string_ord (pairself nickname_of (swap thp))
+ | ord => ord
val freezeT = Type.legacy_freeze_type