--- a/src/HOL/Tools/SMT/verit_isar.ML Tue Sep 30 11:34:20 2014 +0200
+++ b/src/HOL/Tools/SMT/verit_isar.ML Tue Sep 30 12:47:15 2014 +0200
@@ -25,7 +25,7 @@
open VeriT_Proof
fun atp_proof_of_veriT_proof ctxt ll_defs rewrite_rules hyp_ts concl_t fact_helper_ts prem_ids
- conjecture_id fact_helper_ids proof =
+ conjecture_id fact_helper_ids =
let
fun steps_of (VeriT_Proof.VeriT_Step {id, rule, prems, concl, ...}) =
let
@@ -56,7 +56,7 @@
[standard_step Plain]
end
in
- maps steps_of proof
+ maps steps_of
end
end;