diff -r d4cec24a1d87 -r c6b15fc78f78 src/HOL/ex/veriT_Preprocessing.thy
--- a/src/HOL/ex/veriT_Preprocessing.thy	Thu Nov 01 12:23:54 2018 +0100
+++ b/src/HOL/ex/veriT_Preprocessing.thy	Thu Nov 01 14:36:19 2018 +0100
@@ -475,7 +475,7 @@
      [N (Let [@{term "vr1 :: nat"}], [N (Refl, []), N (Refl, [])]),
       N (Let [@{term "vr2 :: nat"}], [N (Refl, []), N (Refl, [])])]));
 
-reconstruct_proof @{context} proof18
+reconstruct_proof @{context} proof25
 \<close>
 
 end