diff -r fc8419fd4735 -r a96ac4d180b7 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Mon Dec 20 08:55:36 2010 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Mon Dec 20 12:12:35 2010 +0100
@@ -12,7 +12,7 @@
   type atp_config =
     {exec: string * string,
      required_execs: (string * string) list,
-     arguments: bool -> Time.time -> string,
+     arguments: bool -> Time.time -> (unit -> (string * real) list) -> string,
      has_incomplete_mode: bool,
      proof_delims: (string * string) list,
      known_failures: (failure * string) list,
@@ -20,6 +20,11 @@
      explicit_forall: bool,
      use_conjecture_for_hypotheses: bool}
 
+  (* for experimentation purposes -- do not use in production code *)
+  val e_generate_weights : bool Unsynchronized.ref
+  val e_weight_factor : real Unsynchronized.ref
+  val e_default_weight : real Unsynchronized.ref
+
   val eN : string
   val spassN : string
   val vampireN : string
@@ -44,7 +49,7 @@
 type atp_config =
   {exec: string * string,
    required_execs: (string * string) list,
-   arguments: bool -> Time.time -> string,
+   arguments: bool -> Time.time -> (unit -> (string * real) list) -> string,
    has_incomplete_mode: bool,
    proof_delims: (string * string) list,
    known_failures: (failure * string) list,
@@ -94,12 +99,28 @@
 val tstp_proof_delims =
   ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation")
 
+val e_generate_weights = Unsynchronized.ref false
+val e_weight_factor = Unsynchronized.ref 4.0
+val e_default_weight = Unsynchronized.ref 0.5
+
+fun e_weights weights =
+  if !e_generate_weights then
+    "(1*FunWeight(ConstPrio," ^
+    string_of_int (Real.ceil (!e_default_weight * !e_weight_factor)) ^
+    ",1,1.5,1.5,1.5" ^
+    (weights ()
+     |> map (fn (s, w) => "," ^ s ^ ":" ^
+                          string_of_int (Real.ceil (w * !e_weight_factor)))
+     |> implode) ^ ")+5*AutoDev)"
+  else
+    "AutoDev"
+
 val e_config : atp_config =
   {exec = ("E_HOME", "eproof"),
    required_execs = [],
-   arguments = fn _ => fn timeout =>
-     "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev --silent \
-     \--cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout),
+   arguments = fn _ => fn timeout => fn weights =>
+     "--tstp-in --tstp-out -l5 -x'" ^ e_weights weights ^ "' -tAutoDev \
+     \--silent --cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout),
    has_incomplete_mode = false,
    proof_delims = [tstp_proof_delims],
    known_failures =
@@ -125,7 +146,7 @@
 val spass_config : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/spass"),
    required_execs = [("SPASS_HOME", "SPASS"), ("SPASS_HOME", "tptp2dfg")],
-   arguments = fn complete => fn timeout =>
+   arguments = fn complete => fn timeout => fn _ =>
      ("-Auto -PGiven=0 -PProblem=0 -Splits=0 -FullRed=0 -DocProof \
       \-VarWeight=3 -TimeLimit=" ^ string_of_int (to_secs 0 timeout))
      |> not complete ? prefix "-SOS=1 ",
@@ -152,7 +173,7 @@
 val vampire_config : atp_config =
   {exec = ("VAMPIRE_HOME", "vampire"),
    required_execs = [],
-   arguments = fn complete => fn timeout =>
+   arguments = fn complete => fn timeout => fn _ =>
      (* This would work too but it's less tested: "--proof tptp " ^ *)
      "--mode casc -t " ^ string_of_int (to_secs 0 timeout) ^
      " --thanks \"Andrei and Krystof\" --input_file"
@@ -214,7 +235,7 @@
                   : atp_config =
   {exec = ("ISABELLE_ATP", "scripts/remote_atp"),
    required_execs = [],
-   arguments = fn _ => fn timeout =>
+   arguments = fn _ => fn timeout => fn _ =>
      " -t " ^ string_of_int (Int.min (max_remote_secs, (to_secs 0 timeout)))
      ^ " -s " ^ the_system system_name system_versions,
    has_incomplete_mode = false,