--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Dec 09 17:26:08 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Dec 10 09:18:17 2010 +0100
@@ -267,8 +267,8 @@
val important_message_keep_factor = 0.1
fun run_atp auto atp_name
- {exec, required_execs, arguments, has_incomplete_mode, proof_delims,
- known_failures, explicit_forall, use_conjecture_for_hypotheses, ...}
+ ({exec, required_execs, arguments, has_incomplete_mode, proof_delims,
+ known_failures, explicit_forall, use_conjecture_for_hypotheses, ...} : atp_config)
({debug, verbose, overlord, full_types, explicit_apply, isar_proof,
isar_shrink_factor, timeout, ...} : params)
minimize_command ({state, goal, subgoal, facts, ...} : prover_problem) =