--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 07 13:03:50 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 07 14:29:18 2012 +0200
@@ -170,7 +170,7 @@
let val thy = Proof_Context.theory_of ctxt in
case try (get_atp thy) name of
SOME config =>
- exists (fn (_, (_, ((_, format, _, _, _), _))) => is_format format)
+ exists (fn (_, ((_, format, _, _, _), _)) => is_format format)
(#best_slices (config ()) ctxt)
| NONE => false
end
@@ -197,7 +197,7 @@
if is_reconstructor name then
reconstructor_default_max_facts
else if is_atp thy name then
- fold (Integer.max o #1 o fst o snd o snd o snd)
+ fold (Integer.max o #1 o fst o snd o snd)
(get_slices slice (#best_slices (get_atp thy name ()) ctxt)) 0
else (* is_smt_prover ctxt name *)
SMT_Solver.default_max_relevant ctxt name
@@ -709,10 +709,10 @@
map (pair name o zero_var_indexes o snd) rths)
end
fun run_slice time_left (cache_key, cache_value)
- (slice, (time_frac, (complete,
+ (slice, (time_frac,
(key as (best_max_facts, format, best_type_enc,
best_lam_trans, best_uncurried_aliases),
- extra)))) =
+ extra))) =
let
val num_facts =
length facts |> is_none max_facts ? Integer.min best_max_facts
@@ -787,8 +787,8 @@
|> fst |> split_time
|> (fn accum as (output, _) =>
(accum,
- extract_tstplike_proof_and_outcome verbose complete
- proof_delims known_failures output
+ extract_tstplike_proof_and_outcome verbose proof_delims
+ known_failures output
|>> atp_proof_from_tstplike_proof atp_problem
handle UNRECOGNIZED_ATP_PROOF () =>
([], SOME ProofIncomplete)))