# HG changeset patch
# User krauss
# Date 1291969097 -3600
# Node ID eaefbe8aac1cfaf3f3bf59ae5d65346637564cb0
# Parent  3933a73dbcb3990506125522f3e06a16e6d4f3be
made smlnj happy

diff -r 3933a73dbcb3 -r eaefbe8aac1c src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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) =