diff -r cf8e4b1acd33 -r 4546c9fdd8a7 src/HOL/Tools/SMT2/verit_proof_parse.ML
--- 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 _