# HG changeset patch
# User blanchet
# Date 1643709489 -3600
# Node ID 7d2a5d1f09af8619595066e4fe1d538f70cef58c
# Parent  52b37e8a617b97e4208e9d58ea9f13825dc97b89
guard against duplicate lines in Zipperposition proofs

diff -r 52b37e8a617b -r 7d2a5d1f09af src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 01 09:21:50 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Feb 01 10:58:09 2022 +0100
@@ -188,7 +188,8 @@
 
             val atp_proof = atp_proof0
               |> trace ? tap (tracing o prefix "atp_proof0 = " o string_of_atp_steps)
-              |> (fn x => fold_rev add_line_pass1 x [])
+              |> distinct (op =)  (* Zipperposition generates duplicate lines *)
+              |> (fn lines => fold_rev add_line_pass1 lines [])
               |> add_lines_pass2 []
               |> trace ? tap (tracing o prefix "atp_proof = " o string_of_atp_steps)