# HG changeset patch
# User blanchet
# Date 1403782382 -7200
# Node ID 9801e9fa9270d45904893fec375c60b6698640d9
# Parent  29691e2dde9a2c230aedca2684460d0c0614e1ea
avoid parallelism, since it confuses the global state and leads to cheating (with 'sml_xxx' engines)

diff -r 29691e2dde9a -r 9801e9fa9270 src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Thu Jun 26 13:32:56 2014 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Thu Jun 26 13:33:02 2014 +0200
@@ -138,7 +138,7 @@
       else
         ""
 
-    val lines = Par_List.map do_fact (tag_list 1 facts)
+    val lines = map do_fact (tag_list 1 facts)
   in
     File.write_list path lines
   end
@@ -213,7 +213,7 @@
     val hd_const_tabs = fold (add_const_counts o prop_of o snd) old_facts Symtab.empty
     val (const_tabs, _) =
       fold_map (`I oo add_const_counts o prop_of o snd o snd o snd) new_facts hd_const_tabs
-    val lines = Par_List.map do_fact (tag_list 1 (new_facts ~~ prevss ~~ const_tabs))
+    val lines = map do_fact (tag_list 1 (new_facts ~~ prevss ~~ const_tabs))
   in
     File.write_list path lines
   end
@@ -260,7 +260,7 @@
 
     fun accum x (yss as ys :: _) = (x :: ys) :: yss
     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)))
+    val lines = map do_fact (tag_list 1 (new_facts ~~ rev (map rev old_factss)))
   in
     File.write_list path lines
   end