--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Nov 19 10:53:22 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML Fri Nov 19 11:04:53 2021 +0100
@@ -72,7 +72,7 @@
val TX0 = TFF (Monomorphic, With_FOOL {with_ite = true, with_let = true})
val TX1 = TFF (Polymorphic, With_FOOL {with_ite = true, with_let = true})
val TH0 = THF (Monomorphic, {with_ite = true, with_let = true}, THF_With_Choice)
-val TH1 = THF (Monomorphic, {with_ite = true, with_let = true}, THF_With_Choice)
+val TH1 = THF (Polymorphic, {with_ite = true, with_let = true}, THF_With_Choice)
val default_max_mono_iters = 3 (* FUDGE *)
val default_max_new_mono_instances = 100 (* FUDGE *)
@@ -680,7 +680,7 @@
val dummy_thf_reduced =
let
- val format = THF (Monomorphic, {with_ite = false, with_let = false}, THF_Without_Choice)
+ val format = THF (Polymorphic, {with_ite = false, with_let = false}, THF_Without_Choice)
val config = dummy_config Hypothesis format "poly_native_higher" false
in (dummy_thfN ^ "_reduced", fn () => config) end