avoid parallelism, since it confuses the global state and leads to cheating (with 'sml_xxx' engines)
authorblanchet
Thu, 26 Jun 2014 13:33:02 +0200
changeset 57352 9801e9fa9270
parent 57351 29691e2dde9a
child 57353 ee493eb30c7b
avoid parallelism, since it confuses the global state and leads to cheating (with 'sml_xxx' engines)
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