--- a/src/HOL/Tools/SMT/smt_systems.ML Tue Sep 30 11:19:30 2014 +0200
+++ b/src/HOL/Tools/SMT/smt_systems.ML Tue Sep 30 11:34:20 2014 +0200
@@ -112,7 +112,7 @@
default_max_relevant = 120 (* FUDGE *),
outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat"
"warning : proof_done: status is still open"),
- parse_proof = SOME VeriT_Proof_Parse.parse_proof,
+ parse_proof = SOME (K VeriT_Proof_Parse.parse_proof),
replay = NONE }
(* Z3 *)
--- a/src/HOL/Tools/SMT/verit_proof_parse.ML Tue Sep 30 11:19:30 2014 +0200
+++ b/src/HOL/Tools/SMT/verit_proof_parse.ML Tue Sep 30 11:34:20 2014 +0200
@@ -8,7 +8,7 @@
signature VERIT_PROOF_PARSE =
sig
type ('a, 'b) atp_step = ('a, 'b) ATP_Proof.atp_step
- val parse_proof: Proof.context -> SMT_Translate.replay_data ->
+ val parse_proof: SMT_Translate.replay_data ->
((string * ATP_Problem_Generate.stature) * thm) list -> term list -> term -> string list ->
SMT_Solver.parsed_proof
end;
@@ -30,7 +30,7 @@
VeriT_Proof.VeriT_Step {id = SMTLIB_Interface.assert_name_of_index i, rule = veriT_input_rule,
prems = [], concl = prop_of th, fixes = []}
-fun parse_proof _
+fun parse_proof
({context = ctxt, typs, terms, ll_defs, rewrite_rules, assms} : SMT_Translate.replay_data)
xfacts prems concl output =
let