src/HOL/Tools/ATP/atp_satallax.ML
changeset 72398 5d1a7b688f6d
parent 70930 1019b8609552
--- 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