# 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>