# HG changeset patch
# User wenzelm
# Date 1718014074 -7200
# Node ID dca37c6479e3462d09980cbf0b2ec949a9b1f46f
# Parent  594356f1681084df2a44db34dd61172f839eeffc
more accurate treatment of Thm_Name.T;

diff -r 594356f16810 -r dca37c6479e3 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sun Jun 09 22:40:13 2024 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Mon Jun 10 12:07:54 2024 +0200
@@ -223,7 +223,7 @@
 
 fun is_that_fact th =
   exists_subterm (fn Free (s, _) => s = skolem_thesis | _ => false) (Thm.prop_of th)
-  andalso String.isSuffix sep_that (Thm_Name.short (Thm.get_name_hint th))
+  andalso String.isSuffix sep_that (#1 (Thm.get_name_hint th))
 
 datatype interest = Deal_Breaker | Interesting | Boring