selectable prover for sledgehammer, proper environment lookup

--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Aug 28 18:23:24 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Aug 28 19:57:12 2009 +0200
@@ -5,9 +5,12 @@
 structure Mirabelle_Sledgehammer : MIRABELLE_ACTION =
 struct
 
-fun sledgehammer_action {pre=st, ...} =
+fun sledgehammer_action args {pre=st, ...} =
   let
-    val prover_name = hd (space_explode " " (AtpManager.get_atps ()))
+    val prover_name =
+      AList.lookup (op =) args "prover"
+      |> the_default (hd (space_explode " " (AtpManager.get_atps ())))
+
     val thy = Proof.theory_of st
  
     val prover = the (AtpManager.get_prover prover_name thy)
@@ -26,6 +29,6 @@
     else NONE
   end
 
-fun invoke _ = Mirabelle.register ("sledgehammer", sledgehammer_action)
+fun invoke args = Mirabelle.register ("sledgehammer", sledgehammer_action args)
 
 end

--- a/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Fri Aug 28 18:23:24 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Fri Aug 28 19:57:12 2009 +0200
@@ -125,7 +125,7 @@
 print LOG_FILE "\n\n";
 close(LOG_FILE);
 
-my $r = system "\"$ISABELLE_PROCESS\" " .
+my $r = system "\"$ENV{'ISABELLE_PROCESS'}\" " .
   "-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n";