Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Decision_Procs/Conversions.thy
changeset 80636 4041e7c8059d
parent 78100 35439ca0133c 
--- a/src/HOL/Decision_Procs/Conversions.thy	Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/Decision_Procs/Conversions.thy	Sun Aug 04 17:39:47 2024 +0200
@@ -24,7 +24,7 @@
   \<open>convert equality to meta equality\<close>
 
 ML \<open>
-fun strip_app ct = ct |> Drule.strip_comb |>> Thm.term_of |>> dest_Const |>> fst;
+fun strip_app ct = ct |> Drule.strip_comb |>> Thm.term_of |>> dest_Const_name;
 
 fun inst cTs cts th =
   Thm.instantiate' (map SOME cTs) (map SOME cts) th;
isabelle