added "overlord" option (to get easy access to output files for debugging) + systematically use "raw_goal" rather than an inconsistent mixture

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Apr 14 18:23:51 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Apr 14 21:22:13 2010 +0200
@@ -12,6 +12,7 @@
   type params =
     {debug: bool,
      verbose: bool,
+     overlord: bool,
      atps: string list,
      full_types: bool,
      respect_no_atp: bool,
@@ -64,6 +65,7 @@
 type params =
   {debug: bool,
    verbose: bool,
+   overlord: bool,
    atps: string list,
    full_types: bool,
    respect_no_atp: bool,

--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Apr 14 18:23:51 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Apr 14 21:22:13 2010 +0200
@@ -120,7 +120,7 @@
                       " theorem" ^ plural_s num_theorems ^ "...")
     val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
     val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
-    val {context = ctxt, facts, goal} = Proof.goal state
+    val {context = ctxt, facts, goal} = Proof.raw_goal state
     val problem =
      {subgoal = subgoal, goal = (ctxt, (facts, goal)),
       relevance_override = {add = [], del = [], only = false},

--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 14 18:23:51 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 14 21:22:13 2010 +0200
@@ -65,8 +65,8 @@
           else SOME "Ill-formed ATP output"
   | (failure :: _) => SOME failure
 
-fun generic_prover get_facts prepare write cmd args failure_strs produce_answer
-        name ({full_types, ...} : params)
+fun generic_prover overlord get_facts prepare write cmd args failure_strs
+        produce_answer name ({full_types, ...} : params)
         ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
          : problem) =
   let
@@ -87,11 +87,15 @@
       prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy;
 
     (* path to unique problem file *)
-    val destdir' = Config.get ctxt destdir;
+    val destdir' = if overlord then getenv "ISABELLE_HOME_USER"
+                   else Config.get ctxt destdir;
     val problem_prefix' = Config.get ctxt problem_prefix;
     fun prob_pathname nr =
-      let val probfile =
-        Path.basic (problem_prefix' ^ serial_string () ^ "_" ^ string_of_int nr)
+      let
+        val probfile =
+          Path.basic (problem_prefix' ^
+                      (if overlord then "_" ^ name else serial_string ())
+                      ^ "_" ^ string_of_int nr)
       in
         if destdir' = "" then File.tmp_path probfile
         else if File.exists (Path.explode destdir')
@@ -159,11 +163,11 @@
 fun generic_tptp_prover
         (name, {command, arguments, failure_strs, max_new_clauses,
                 prefers_theory_const, supports_isar_proofs})
-        (params as {respect_no_atp, relevance_threshold, convergence,
+        (params as {overlord, respect_no_atp, relevance_threshold, convergence,
                     theory_const, higher_order, follow_defs, isar_proof,
                     modulus, sorts, ...})
         timeout =
-  generic_prover
+  generic_prover overlord
       (get_relevant_facts respect_no_atp relevance_threshold convergence
                           higher_order follow_defs max_new_clauses
                           (the_default prefers_theory_const theory_const))
@@ -219,10 +223,10 @@
 fun generic_dfg_prover
         (name, ({command, arguments, failure_strs, max_new_clauses,
                  prefers_theory_const, ...} : prover_config))
-        (params as {respect_no_atp, relevance_threshold, convergence,
+        (params as {overlord, respect_no_atp, relevance_threshold, convergence,
                     theory_const, higher_order, follow_defs, ...})
         timeout =
-  generic_prover
+  generic_prover overlord
       (get_relevant_facts respect_no_atp relevance_threshold convergence
                           higher_order follow_defs max_new_clauses
                           (the_default prefers_theory_const theory_const))

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 14 18:23:51 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 14 21:22:13 2010 +0200
@@ -40,6 +40,7 @@
 val default_default_params =
   [("debug", "false"),
    ("verbose", "false"),
+   ("overlord", "false"),
    ("respect_no_atp", "true"),
    ("relevance_threshold", "50"),
    ("convergence", "320"),
@@ -56,6 +57,7 @@
 val negated_alias_params =
   [("no_debug", "debug"),
    ("quiet", "verbose"),
+   ("no_overlord", "overlord"),
    ("ignore_no_atp", "respect_no_atp"),
    ("partial_types", "full_types"),
    ("no_theory_const", "theory_const"),
@@ -133,6 +135,7 @@
                                    " must be assigned an integer value.")
     val debug = lookup_bool "debug"
     val verbose = debug orelse lookup_bool "verbose"
+    val overlord = lookup_bool "overlord"
     val atps = lookup_string "atps" |> space_explode " "
     val full_types = lookup_bool "full_types"
     val respect_no_atp = lookup_bool "respect_no_atp"
@@ -148,12 +151,12 @@
     val timeout = lookup_time "timeout"
     val minimize_timeout = lookup_time "minimize_timeout"
   in
-    {debug = debug, verbose = verbose, atps = atps, full_types = full_types,
-     respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
-     convergence = convergence, theory_const = theory_const,
-     higher_order = higher_order, follow_defs = follow_defs,
-     isar_proof = isar_proof, modulus = modulus, sorts = sorts,
-     timeout = timeout, minimize_timeout = minimize_timeout}
+    {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
+     full_types = full_types, respect_no_atp = respect_no_atp,
+     relevance_threshold = relevance_threshold, convergence = convergence,
+     theory_const = theory_const, higher_order = higher_order,
+     follow_defs = follow_defs, isar_proof = isar_proof, modulus = modulus,
+     sorts = sorts, timeout = timeout, minimize_timeout = minimize_timeout}
   end
 
 fun get_params thy = extract_params thy (default_raw_params thy)