changed order of facts so that 'name_tabs' has the same order everywhere (which affects unaliasing)
--- a/src/HOL/TPTP/mash_export.ML Tue Jun 24 08:19:58 2014 +0200
+++ b/src/HOL/TPTP/mash_export.ML Tue Jun 24 08:20:00 2014 +0200
@@ -254,8 +254,8 @@
""
fun accum x (yss as ys :: _) = (x :: ys) :: yss
- val old_factss = tl (fold accum new_facts [old_facts])
- val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ rev old_factss))
+ val old_factss = tl (fold accum new_facts [rev old_facts])
+ val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ rev (map rev old_factss)))
in
File.write_list path lines
end