# HG changeset patch
# User desharna
# Date 1637316293 -3600
# Node ID b605ebd87a4748d15899c68da9ea975873ca9fd8
# Parent  a64a8f7d593e077c82720c1d0831b86ed43157ce
proper polymorphism for TH1 format in Sledgehammer

diff -r a64a8f7d593e -r b605ebd87a47 src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- 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