# HG changeset patch
# User wenzelm
# Date 1348493878 -7200
# Node ID 3b0a60eee56e4c77301ce97b7ba34e5a96705987
# Parent  8192dc55bda9b7ab0178752faa4233c7e3c2338c
Mirabelle appears to work better in single-threaded mode;

diff -r 8192dc55bda9 -r 3b0a60eee56e src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Sep 24 14:22:07 2012 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Mon Sep 24 15:37:58 2012 +0200
@@ -157,7 +157,7 @@
 if ($output_log) { print "Mirabelle: $thy_file\n"; }
 
 my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
-  "-e 'Unsynchronized.setmp quick_and_dirty true use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
+  "-e 'Unsynchronized.setmp Multithreading.max_threads 1 (Unsynchronized.setmp quick_and_dirty true use_thy) \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet;
 
 if ($output_log) {
   my $outcome = ($result ? "failure" : "success");