diff -r c1cca2a052e4 -r 81c3c4e01263 src/HOL/Mirabelle/lib/scripts/mirabelle.pl --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Tue Apr 24 09:09:55 2012 +0200 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Tue Apr 24 09:47:40 2012 +0200 @@ -138,7 +138,7 @@ if ($output_log) { print "Mirabelle: $thy_file\n"; } my $result = system "\"$ENV{'ISABELLE_PROCESS'}\" " . - "-e 'use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet; + "-e 'Unsynchronized.setmp quick_and_dirty true use_thy \"$path/$new_thy_name\" handle _ => exit 1;\n' -q $mirabelle_logic" . $quiet; if ($output_log) { print "Finished: $thy_file\n"; }