src/HOL/Tools/ATP/atp_systems.ML

                 else combsN, uncurried_aliases), ""))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 
 val dummy_thf_format = THF (Polymorphic, THF_With_Choice)
+
 val dummy_thf_config = dummy_config Hypothesis dummy_thf_format "poly_native_higher" false
 val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
+
+val dummy_thf_ml_config = dummy_config Hypothesis dummy_thf_format "ml_poly_native_higher" false
+val dummy_thf_ml = (dummy_thf_mlN, fn () => dummy_thf_ml_config)
 
 val spass_pirate_format = DFG Polymorphic
 val remote_spass_pirate_config : atp_config =
   {exec = K (["ISABELLE_ATP"], ["scripts/remote_spass_pirate"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>

       end
   end
 
 val atps =
   [agsyhol, alt_ergo, e, e_males, e_par, iprover, iprover_eq, leo2, satallax, spass, vampire,
-   z3_tptp, zipperposition, dummy_thf, remote_agsyhol, remote_e, remote_e_sine, remote_e_tofof,
-   remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire, remote_snark,
-   remote_spass_pirate, remote_waldmeister, remote_waldmeister_new]
+   z3_tptp, zipperposition, dummy_thf, dummy_thf_ml, remote_agsyhol, remote_e, remote_e_sine,
+   remote_e_tofof, remote_iprover, remote_iprover_eq, remote_leo2, remote_satallax, remote_vampire,
+   remote_snark, remote_spass_pirate, remote_waldmeister, remote_waldmeister_new]
 
 val _ = Theory.setup (fold add_atp atps)
 
 end;