--- 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"