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