# HG changeset patch
# User blanchet
# Date 1355778388 -3600
# Node ID 001a0e12d7f1eaf936e97ce4bf2ecc05bcab1617
# Parent  0eaefd4306d7537bb1b8e7d565062e6f5a0fcad2
tuned order to help debugging

diff -r 0eaefd4306d7 -r 001a0e12d7f1 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Mon Dec 17 18:23:08 2012 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Mon Dec 17 22:06:28 2012 +0100
@@ -97,7 +97,8 @@
         val name = nickname_of th
         val feats =
           features_of ctxt prover (theory_of_thm th) stature [prop_of th]
-        val s = escape_meta name ^ ": " ^ encode_features feats ^ "\n"
+        val s =
+          escape_meta name ^ ": " ^ encode_features (sort_wrt fst feats) ^ "\n"
       in File.append path s end
   in List.app do_fact facts end
 
@@ -163,7 +164,7 @@
                                            (SOME isar_deps)
           val core =
             escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
-            encode_features feats
+            encode_features (sort_wrt fst feats)
           val query =
             if is_bad_query ctxt ho_atp th (these isar_deps) then ""
             else "? " ^ core ^ "\n"