# HG changeset patch
# User wenzelm
# Date 1348496036 -7200
# Node ID 0a82e98fd4a30478381c2bc200cd03ca556992e1
# Parent  3b0a60eee56e4c77301ce97b7ba34e5a96705987
discontinued futile attempt to hardwire build options into the image, sequential mode is enabled more robustly at runtime (cf. 3b0a60eee56e);

diff -r 3b0a60eee56e -r 0a82e98fd4a3 src/HOL/Mirabelle/Mirabelle.thy
--- a/src/HOL/Mirabelle/Mirabelle.thy	Mon Sep 24 15:37:58 2012 +0200
+++ b/src/HOL/Mirabelle/Mirabelle.thy	Mon Sep 24 16:13:56 2012 +0200
@@ -9,10 +9,6 @@
 ML_file "Tools/mirabelle.ML"
 ML_file "../TPTP/sledgehammer_tactics.ML"
 
-(* no multithreading, no parallel proofs *)  (* FIXME *)
-ML {* Multithreading.max_threads := 1 *}
-ML {* Goal.parallel_proofs := 0 *}
-
 ML {* Toplevel.add_hook Mirabelle.step_hook *}
 
 ML {*