# HG changeset patch
# User blanchet
# Date 1626681800 -7200
# Node ID 943757b788f9abd6d7425ddcdad724c14709f9f8
# Parent  13c66810f7b0e547b6f454d29b1fc75ba22636bd
compile

diff -r 13c66810f7b0 -r 943757b788f9 src/HOL/TPTP/atp_theory_export.ML
--- a/src/HOL/TPTP/atp_theory_export.ML	Sun Jul 18 22:13:36 2021 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML	Mon Jul 19 10:03:20 2021 +0200
@@ -38,7 +38,6 @@
 
 fun atp_of_format (THF (_, Polymorphic, _)) = leo3N
   | atp_of_format (THF (_, Monomorphic, _)) = satallaxN
-  | atp_of_format (DFG Polymorphic) = pirateN
   | atp_of_format (DFG Monomorphic) = spassN
   | atp_of_format (TFF (_, Polymorphic)) = alt_ergoN
   | atp_of_format (TFF (_, Monomorphic)) = vampireN