# HG changeset patch
# User blanchet
# Date 1403590800 -7200
# Node ID 2ccd6820f74e9090edf32ae0a03058c7df04ecaf
# Parent  ef9d4e1ceb00a3ab83d327538f188aa74f5ed7f7
changed order of facts so that 'name_tabs' has the same order everywhere (which affects unaliasing)

diff -r ef9d4e1ceb00 -r 2ccd6820f74e src/HOL/TPTP/mash_export.ML
--- 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