--- a/src/HOL/Tools/SMT2/verit_proof_parse.ML Wed Jul 30 14:03:13 2014 +0200
+++ b/src/HOL/Tools/SMT2/verit_proof_parse.ML Wed Jul 30 14:03:58 2014 +0200
@@ -68,8 +68,8 @@
fun add_missing_steps iidths =
let
- fun add_single_step (_, (id, th)) = VeriT_Proof.VeriT_Step {id = string_of_int id, rule = "input",
- prems = [], concl = prop_of th, fixes = []}
+ fun add_single_step (_, (id, th)) = VeriT_Proof.VeriT_Step {id = string_of_int id,
+ rule = veriT_input_rule, prems = [], concl = prop_of th, fixes = []}
in map add_single_step iidths end
fun parse_proof _