# 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)