compile

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