diff -r 2463cba9f18f -r f54c32c413a9 src/HOL/Mirabelle/lib/scripts/mirabelle.pl --- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Tue Jun 20 21:41:59 2017 +0200 +++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Wed Jun 21 22:48:55 2017 +0200 @@ -10,6 +10,7 @@ my $isabelle_home = $ENV{'ISABELLE_HOME'}; my $mirabelle_home = $ENV{'MIRABELLE_HOME'}; +my $mirabelle_dir = $ENV{'MIRABELLE_DIR'}; my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'}; my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'}; my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'}; @@ -160,7 +161,9 @@ my $cmd = "isabelle process -o quick_and_dirty -o threads=1" . - " -T \"$path/$new_thy_name\" -l $mirabelle_logic" . $quiet; + " -T \"$path/$new_thy_name\" " . + ($mirabelle_dir ? "-d " . $mirabelle_dir . " " : "") . + "-l $mirabelle_logic" . $quiet; my $result = system "bash", "-c", $cmd; if ($output_log) {