--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Fri Aug 01 14:43:57 2014 +0200
@@ -385,8 +385,7 @@
minimize, atp_proof, goal)
end
- val one_line_params =
- (preplay, proof_banner mode name, used_facts, subgoal, subgoal_count)
+ val one_line_params = (preplay, proof_banner mode name, subgoal, subgoal_count)
val num_chained = length (#facts (Proof.goal state))
in
proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained