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