# HG changeset patch
# User desharna
# Date 1628058436 -7200
# Node ID 58e208ad4bcf563c408c4fecacb7869971beafa3
# Parent  6c7feeef0ff237a19ad2afe0c762ce2dd69122a8# Parent  3146646a43a7961d74854a8bb98981f41faa572f
merged

diff -r 3146646a43a7 -r 58e208ad4bcf NEWS
--- a/NEWS	Tue Aug 03 13:53:22 2021 +0000
+++ b/NEWS	Wed Aug 04 08:27:16 2021 +0200
@@ -201,7 +201,7 @@
 INCOMPATIBILITY.
 
 * Sledgehammer:
- - Removed legacy "lam_lifting" (synonym for "liftinng") from option
+ - Removed legacy "lam_lifting" (synonym for "lifting") from option
    "lam_trans". Minor INCOMPATIBILITY.
  - Renamed "hide_lams" to "opaque_lifting" in option "lam_trans".
    Minor INCOMPATIBILITY.
diff -r 3146646a43a7 -r 58e208ad4bcf src/HOL/Tools/ATP/atp_proof.ML
--- a/src/HOL/Tools/ATP/atp_proof.ML	Tue Aug 03 13:53:22 2021 +0000
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Wed Aug 04 08:27:16 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 3146646a43a7 -r 58e208ad4bcf src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Tue Aug 03 13:53:22 2021 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Aug 04 08:27:16 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)