1.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Apr 14 18:23:51 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Apr 14 21:22:13 2010 +0200
     1.3 @@ -12,6 +12,7 @@
     1.4    type params =
     1.5      {debug: bool,
     1.6       verbose: bool,
     1.7 +     overlord: bool,
     1.8       atps: string list,
     1.9       full_types: bool,
    1.10       respect_no_atp: bool,
    1.11 @@ -64,6 +65,7 @@
    1.12  type params =
    1.13    {debug: bool,
    1.14     verbose: bool,
    1.15 +   overlord: bool,
    1.16     atps: string list,
    1.17     full_types: bool,
    1.18     respect_no_atp: bool,

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

     3.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 14 18:23:51 2010 +0200
     3.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 14 21:22:13 2010 +0200
     3.3 @@ -65,8 +65,8 @@
     3.4            else SOME "Ill-formed ATP output"
     3.5    | (failure :: _) => SOME failure
     3.6  
     3.7 -fun generic_prover get_facts prepare write cmd args failure_strs produce_answer
     3.8 -        name ({full_types, ...} : params)
     3.9 +fun generic_prover overlord get_facts prepare write cmd args failure_strs
    3.10 +        produce_answer name ({full_types, ...} : params)
    3.11          ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
    3.12           : problem) =
    3.13    let
    3.14 @@ -87,11 +87,15 @@
    3.15        prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy;
    3.16  
    3.17      (* path to unique problem file *)
    3.18 -    val destdir' = Config.get ctxt destdir;
    3.19 +    val destdir' = if overlord then getenv "ISABELLE_HOME_USER"
    3.20 +                   else Config.get ctxt destdir;
    3.21      val problem_prefix' = Config.get ctxt problem_prefix;
    3.22      fun prob_pathname nr =
    3.23 -      let val probfile =
    3.24 -        Path.basic (problem_prefix' ^ serial_string () ^ "_" ^ string_of_int nr)
    3.25 +      let
    3.26 +        val probfile =
    3.27 +          Path.basic (problem_prefix' ^
    3.28 +                      (if overlord then "_" ^ name else serial_string ())
    3.29 +                      ^ "_" ^ string_of_int nr)
    3.30        in
    3.31          if destdir' = "" then File.tmp_path probfile
    3.32          else if File.exists (Path.explode destdir')
    3.33 @@ -159,11 +163,11 @@
    3.34  fun generic_tptp_prover
    3.35          (name, {command, arguments, failure_strs, max_new_clauses,
    3.36                  prefers_theory_const, supports_isar_proofs})
    3.37 -        (params as {respect_no_atp, relevance_threshold, convergence,
    3.38 +        (params as {overlord, respect_no_atp, relevance_threshold, convergence,
    3.39                      theory_const, higher_order, follow_defs, isar_proof,
    3.40                      modulus, sorts, ...})
    3.41          timeout =
    3.42 -  generic_prover
    3.43 +  generic_prover overlord
    3.44        (get_relevant_facts respect_no_atp relevance_threshold convergence
    3.45                            higher_order follow_defs max_new_clauses
    3.46                            (the_default prefers_theory_const theory_const))
    3.47 @@ -219,10 +223,10 @@
    3.48  fun generic_dfg_prover
    3.49          (name, ({command, arguments, failure_strs, max_new_clauses,
    3.50                   prefers_theory_const, ...} : prover_config))
    3.51 -        (params as {respect_no_atp, relevance_threshold, convergence,
    3.52 +        (params as {overlord, respect_no_atp, relevance_threshold, convergence,
    3.53                      theory_const, higher_order, follow_defs, ...})
    3.54          timeout =
    3.55 -  generic_prover
    3.56 +  generic_prover overlord
    3.57        (get_relevant_facts respect_no_atp relevance_threshold convergence
    3.58                            higher_order follow_defs max_new_clauses
    3.59                            (the_default prefers_theory_const theory_const))

     4.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 14 18:23:51 2010 +0200
     4.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Apr 14 21:22:13 2010 +0200
     4.3 @@ -40,6 +40,7 @@
     4.4  val default_default_params =
     4.5    [("debug", "false"),
     4.6     ("verbose", "false"),
     4.7 +   ("overlord", "false"),
     4.8     ("respect_no_atp", "true"),
     4.9     ("relevance_threshold", "50"),
    4.10     ("convergence", "320"),
    4.11 @@ -56,6 +57,7 @@
    4.12  val negated_alias_params =
    4.13    [("no_debug", "debug"),
    4.14     ("quiet", "verbose"),
    4.15 +   ("no_overlord", "overlord"),
    4.16     ("ignore_no_atp", "respect_no_atp"),
    4.17     ("partial_types", "full_types"),
    4.18     ("no_theory_const", "theory_const"),
    4.19 @@ -133,6 +135,7 @@
    4.20                                     " must be assigned an integer value.")
    4.21      val debug = lookup_bool "debug"
    4.22      val verbose = debug orelse lookup_bool "verbose"
    4.23 +    val overlord = lookup_bool "overlord"
    4.24      val atps = lookup_string "atps" |> space_explode " "
    4.25      val full_types = lookup_bool "full_types"
    4.26      val respect_no_atp = lookup_bool "respect_no_atp"
    4.27 @@ -148,12 +151,12 @@
    4.28      val timeout = lookup_time "timeout"
    4.29      val minimize_timeout = lookup_time "minimize_timeout"
    4.30    in
    4.31 -    {debug = debug, verbose = verbose, atps = atps, full_types = full_types,
    4.32 -     respect_no_atp = respect_no_atp, relevance_threshold = relevance_threshold,
    4.33 -     convergence = convergence, theory_const = theory_const,
    4.34 -     higher_order = higher_order, follow_defs = follow_defs,
    4.35 -     isar_proof = isar_proof, modulus = modulus, sorts = sorts,
    4.36 -     timeout = timeout, minimize_timeout = minimize_timeout}
    4.37 +    {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
    4.38 +     full_types = full_types, respect_no_atp = respect_no_atp,
    4.39 +     relevance_threshold = relevance_threshold, convergence = convergence,
    4.40 +     theory_const = theory_const, higher_order = higher_order,
    4.41 +     follow_defs = follow_defs, isar_proof = isar_proof, modulus = modulus,
    4.42 +     sorts = sorts, timeout = timeout, minimize_timeout = minimize_timeout}
    4.43    end
    4.44  
    4.45  fun get_params thy = extract_params thy (default_raw_params thy)