# HG changeset patch
# User blanchet
# Date 1412065504 -7200
# Node ID 289d1c39968c8ffb34986cdc4a7df89f5c6749a9
# Parent  1ae4ab94ea6384067cb83aca2d5d568b05c6c40d
correct indexing in the presence of lambda-lifting

diff -r 1ae4ab94ea63 -r 289d1c39968c src/HOL/Tools/SMT/verit_proof_parse.ML
--- 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