# HG changeset patch # User wenzelm # Date 1737483969 -3600 # Node ID 23957ebffaf766548779237b1866ef0cbf0d66c7 # Parent 234912588ffe0f783682e11b8a1e29b481fe3013 more robust: explicit check for "Trueprop"; diff -r 234912588ffe -r 23957ebffaf7 src/HOL/Tools/sat.ML --- a/src/HOL/Tools/sat.ML Tue Jan 21 16:59:57 2025 +0100 +++ b/src/HOL/Tools/sat.ML Tue Jan 21 19:26:09 2025 +0100 @@ -165,8 +165,7 @@ val res_thm = let - val P = - snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1)) (* strip Trueprop *) + val P = HOLogic.dest_judgment (if hyp1_is_neg then hyp2 else hyp1) in \<^instantiate>\<open>P in lemma \<open>(P \<Longrightarrow> False) \<Longrightarrow> (\<not> P \<Longrightarrow> False) \<Longrightarrow> False\<close> by (rule case_split)\<close>