# HG changeset patch
# User blanchet
# Date 1280337836 -7200
# Node ID 327705ac47590c1ec7036183bceafa4ec82c0ebd
# Parent  9eda375ec19dbf7d04ff3256d2e9a64577b0b841
renamed environment variable

diff -r 9eda375ec19d -r 327705ac4759 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Jul 28 19:07:34 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Jul 28 19:23:56 2010 +0200
@@ -108,7 +108,7 @@
 (* The "-VarWeight=3" option helps the higher-order problems, probably by
    counteracting the presence of "hAPP". *)
 val spass_config : prover_config =
-  {executable = ("ISABELLE_ATP_MANAGER", "scripts/spass"),
+  {executable = ("ISABELLE_ATP", "scripts/spass"),
    required_executables = [("SPASS_HOME", "SPASS")],
    (* "div 2" accounts for the fact that SPASS is often run twice. *)
    arguments = fn complete => fn timeout =>
@@ -157,7 +157,7 @@
 val systems = Synchronized.var "atp_systems" ([]: string list)
 
 fun get_systems () =
-  case bash_output "\"$ISABELLE_ATP_MANAGER/scripts/remote_atp\" -w" of
+  case bash_output "\"$ISABELLE_ATP/scripts/remote_atp\" -w" of
     (answer, 0) => split_lines answer
   | (answer, _) =>
     error ("Failed to get available systems at SystemOnTPTP:\n" ^
@@ -184,7 +184,7 @@
         ({proof_delims, known_failures, max_new_relevant_facts_per_iter,
           prefers_theory_relevant, explicit_forall, ...} : prover_config)
         : prover_config =
-  {executable = ("ISABELLE_ATP_MANAGER", "scripts/remote_atp"),
+  {executable = ("ISABELLE_ATP", "scripts/remote_atp"),
    required_executables = [],
    arguments = fn _ => fn timeout =>
      " -t " ^ string_of_int (to_generous_secs timeout) ^ " -s " ^
diff -r 9eda375ec19d -r 327705ac4759 src/HOL/Tools/ATP/etc/settings
--- a/src/HOL/Tools/ATP/etc/settings	Wed Jul 28 19:07:34 2010 +0200
+++ b/src/HOL/Tools/ATP/etc/settings	Wed Jul 28 19:23:56 2010 +0200
@@ -1,2 +1,1 @@
-ISABELLE_ATP_MANAGER="$COMPONENT"
-
+ISABELLE_ATP="$COMPONENT"