src/HOL/TPTP/atp_theory_export.ML

   No_Inferences | Unchecked_Inferences | Checked_Inferences
 
 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
   | atp_of_format (TFF Monomorphic) = vampireN
   | atp_of_format FOF = eN