changeset 58488 | 289d1c39968c |
parent 58482 | 7836013951e6 |
child 58491 | 5ddbc170e46c |
--- a/src/HOL/Tools/SMT/verit_proof_parse.ML Mon Sep 29 22:09:17 2014 +0200 +++ b/src/HOL/Tools/SMT/verit_proof_parse.ML Tue Sep 30 10:25:04 2014 +0200 @@ -40,8 +40,8 @@ val assm_steps = map step_of_assm used_assms val steps = assm_steps @ actual_steps - val conjecture_i = 0 - val prems_i = 1 + val conjecture_i = length ll_defs + val prems_i = conjecture_i + 1 val num_prems = length prems val facts_i = prems_i + num_prems val num_facts = length xfacts