Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more accurate treatment of Thm_Name.T;
authorwenzelm
Mon, 10 Jun 2024 12:07:54 +0200
changeset 80325 dca37c6479e3
parent 80314 594356f16810
child 80326 53f12ab896e6
more accurate treatment of Thm_Name.T;
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle