# HG changeset patch
# User wenzelm
# Date 1737472191 -3600
# Node ID 35d243b25ae26d474ab6db6885319123ecf139a0
# Parent  07fefe59ac204a01fc9e5c4b1e7b211d79361297
tuned;

diff -r 07fefe59ac20 -r 35d243b25ae2 src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Tue Jan 21 11:16:48 2025 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Tue Jan 21 16:09:51 2025 +0100
@@ -76,7 +76,7 @@
         (case try_proof ctxt (goals \<^const_name>\<open>Orderings.less_eq\<close>) solve_tac of
           Solved thm2 => LessEq (thm2, thm)
         | Stuck thm2 =>
-            if Thm.prems_of thm2 = [HOLogic.Trueprop $ \<^term>\<open>False\<close>] then False thm2
+            if Thm.prems_of thm2 = [\<^prop>\<open>False\<close>] then False thm2
             else None (thm2, thm)
         | _ => raise Match) (* FIXME *)
     | _ => raise Match)
diff -r 07fefe59ac20 -r 35d243b25ae2 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Tue Jan 21 11:16:48 2025 +0100
+++ b/src/HOL/Tools/Function/termination.ML	Tue Jan 21 16:09:51 2025 +0100
@@ -179,7 +179,7 @@
         (case try \<^const_name>\<open>Orderings.less_eq\<close> of
           Solved thm2 => LessEq (thm2, thm)
         | Stuck thm2 =>
-            if Thm.prems_of thm2 = [HOLogic.Trueprop $ \<^term>\<open>False\<close>]
+            if Thm.prems_of thm2 = [\<^prop>\<open>False\<close>]
             then False thm2 else None (thm2, thm)
         | _ => raise Match) (* FIXME *)
     | _ => raise Match)