# 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