# HG changeset patch
# User desharna
# Date 1627975358 -7200
# Node ID ed1f576df9c4e91454593d807b8a7313f5411f07
# Parent  d3d6e01a6b002929ae2bf6e7771d8ee2f32bc84c
added dummy_thf prover to Sledgehammer

diff -r d3d6e01a6b00 -r ed1f576df9c4 src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Mon Aug 02 17:20:16 2021 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Tue Aug 03 09:22:38 2021 +0200
@@ -55,6 +55,7 @@
   val zipperpositionN : string
   val remote_prefix : string
   val dummy_tfxN : string
+  val dummy_thfN : string
 
   val agsyhol_core_rule : string
   val spass_input_rule : string
@@ -117,6 +118,7 @@
 val zipperpositionN = "zipperposition"
 val remote_prefix = "remote_"
 val dummy_tfxN = "dummy_tfx"
+val dummy_thfN = "dummy_thf"
 
 val agsyhol_core_rule = "__agsyhol_core" (* arbitrary *)
 val spass_input_rule = "Inp"
diff -r d3d6e01a6b00 -r ed1f576df9c4 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Mon Aug 02 17:20:16 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Tue Aug 03 09:22:38 2021 +0200
@@ -682,10 +682,13 @@
    best_max_new_mono_instances = default_max_new_mono_instances}
 
 val dummy_tfx_format = TFF (With_FOOL, Polymorphic)
-
 val dummy_tfx_config = dummy_config Hypothesis dummy_tfx_format "mono_native_fool" false
 val dummy_tfx = (dummy_tfxN, fn () => dummy_tfx_config)
 
+val dummy_thf_format = THF (With_FOOL, Polymorphic, THF_With_Choice)
+val dummy_thf_config = dummy_config Hypothesis dummy_thf_format "mono_native_higher_fool" false
+val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
+
 
 (* Setup *)
 
@@ -722,7 +725,7 @@
 val atps =
   [agsyhol, alt_ergo, e, iprover, leo2, leo3, satallax, spass, vampire, z3_tptp, zipperposition,
    remote_agsyhol, remote_alt_ergo, remote_e, remote_iprover, remote_leo2, remote_leo3,
-   remote_waldmeister, remote_zipperposition, dummy_tfx]
+   remote_waldmeister, remote_zipperposition, dummy_tfx, dummy_thf]
 
 val _ = Theory.setup (fold add_atp atps)