--- a/src/HOL/TPTP/atp_theory_export.ML Thu Nov 12 16:18:43 2020 +0100
+++ b/src/HOL/TPTP/atp_theory_export.ML Thu Nov 12 16:42:22 2020 +0100
@@ -36,12 +36,12 @@
val prefix = Library.prefix
val fact_name_of = prefix fact_prefix o ascii_of
-fun atp_of_format (THF (Polymorphic, _)) = leo3N
- | atp_of_format (THF (Monomorphic, _)) = satallaxN
+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
+ | atp_of_format (TFF (_, Polymorphic)) = alt_ergoN
+ | atp_of_format (TFF (_, Monomorphic)) = vampireN
| atp_of_format FOF = eN (* FIXME? *)
| atp_of_format CNF_UEQ = waldmeisterN
| atp_of_format CNF = eN (* FIXME? *)