# HG changeset patch
# User blanchet
# Date 1354700158 -3600
# Node ID da395f0e7deaa88eebcf55296dfb4125f14482f9
# Parent  b7d3319409b70c83f3cbeeac592d3e8c0b2c20eb
tweaked order of theorems to avoid forward dependencies (MaSh)

diff -r b7d3319409b7 -r da395f0e7dea src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- 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