--- a/src/HOL/Tools/ATP/atp_satallax.ML Thu Oct 08 07:30:02 2020 +0000
+++ b/src/HOL/Tools/ATP/atp_satallax.ML Thu Oct 08 16:07:10 2020 +0200
@@ -56,7 +56,7 @@
fun parse_tstp_thf0_satallax_line x =
(((Scan.this_string tptp_thf
-- $$ "(") |-- scan_general_id --| $$ "," -- Symbol.scan_ascii_id --| $$ ","
- -- parse_thf_formula -- Scan.option parse_tstp_satallax_extra_arguments --| $$ ")" --| $$ ".")
+ -- parse_hol_formula -- Scan.option parse_tstp_satallax_extra_arguments --| $$ ")" --| $$ ".")
|| (Scan.this_string "tab_inh" |-- skip_term --| $$ ".")
>> K dummy_satallax_step) x