# HG changeset patch
# User blanchet
# Date 1412069660 -7200
# Node ID 5ddbc170e46c3e78980b34ab5613b8490ef800d1
# Parent  f6d99c69dae90b1e428b278c342af6c5224d4f42
tuning

diff -r f6d99c69dae9 -r 5ddbc170e46c src/HOL/Tools/SMT/smt_systems.ML
--- 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 *)
diff -r f6d99c69dae9 -r 5ddbc170e46c src/HOL/Tools/SMT/verit_proof_parse.ML
--- 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