tuned order to help debugging
authorblanchet
Mon Dec 17 22:06:28 2012 +0100 (2012-12-17)
changeset 50582001a0e12d7f1
parent 50581 0eaefd4306d7
child 50583 681edd111e9b
tuned order to help debugging
src/HOL/TPTP/mash_export.ML
     1.1 --- a/src/HOL/TPTP/mash_export.ML	Mon Dec 17 18:23:08 2012 +0100
     1.2 +++ b/src/HOL/TPTP/mash_export.ML	Mon Dec 17 22:06:28 2012 +0100
     1.3 @@ -97,7 +97,8 @@
     1.4          val name = nickname_of th
     1.5          val feats =
     1.6            features_of ctxt prover (theory_of_thm th) stature [prop_of th]
     1.7 -        val s = escape_meta name ^ ": " ^ encode_features feats ^ "\n"
     1.8 +        val s =
     1.9 +          escape_meta name ^ ": " ^ encode_features (sort_wrt fst feats) ^ "\n"
    1.10        in File.append path s end
    1.11    in List.app do_fact facts end
    1.12  
    1.13 @@ -163,7 +164,7 @@
    1.14                                             (SOME isar_deps)
    1.15            val core =
    1.16              escape_meta name ^ ": " ^ escape_metas prevs ^ "; " ^
    1.17 -            encode_features feats
    1.18 +            encode_features (sort_wrt fst feats)
    1.19            val query =
    1.20              if is_bad_query ctxt ho_atp th (these isar_deps) then ""
    1.21              else "? " ^ core ^ "\n"