--- a/src/HOL/TPTP/atp_theory_export.ML Thu Oct 24 10:03:20 2013 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Thu Oct 24 12:43:33 2013 +0200
@@ -34,8 +34,8 @@
val prefix = Library.prefix
val fact_name_of = prefix fact_prefix o ascii_of
-fun atp_of_format (THF (Polymorphic, _, _)) = dummy_thfN
- | atp_of_format (THF (Monomorphic, _, _)) = satallaxN
+fun atp_of_format (THF (Polymorphic, _)) = dummy_thfN
+ | atp_of_format (THF (Monomorphic, _)) = satallaxN
| atp_of_format (DFG Polymorphic) = spass_polyN
| atp_of_format (DFG Monomorphic) = spassN
| atp_of_format (TFF Polymorphic) = alt_ergoN