# HG changeset patch
# User desharna
# Date 1614079250 -3600
# Node ID f0210642e43fa0c1db0ca5e11db3c9a0522981fb
# Parent  8b6fa865bac490a5b816c59dd83a65cb0b220c14
proper usage of hypotheses for zipperposition's TPTP generation

diff -r 8b6fa865bac4 -r f0210642e43f src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Tue Feb 23 10:13:09 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Tue Feb 23 12:20:50 2021 +0100
@@ -550,7 +550,7 @@
      |> extra_options <> "" ? prefix (extra_options ^ " "),
    proof_delims = tstp_proof_delims,
    known_failures = known_szs_status_failures,
-   prem_role = Conjecture,
+   prem_role = Hypothesis,
    best_slices = fn _ =>
      (* FUDGE *)
      [(0.333, (((128, "meshN"), THF (Without_FOOL, Polymorphic, THF_Without_Choice), "mono_native_higher", keep_lamsN, false), zipperposition_blsimp)),