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/Pure/Isar/specification.ML
changeset 80635 27d5452d20fc
parent 80632 3a196e63a80d
child 81116 0fb1e2dd4122 
--- a/src/Pure/Isar/specification.ML	Sun Aug 04 13:24:54 2024 +0200
+++ b/src/Pure/Isar/specification.ML	Sun Aug 04 16:56:28 2024 +0200
@@ -319,7 +319,7 @@
 val alias_cmd =
   gen_alias Local_Theory.const_alias
     (fn flags => fn ctxt => fn (c, pos) =>
-      apfst (#1 o dest_Const) (Proof_Context.check_const flags ctxt (c, [pos])));
+      apfst dest_Const_name (Proof_Context.check_const flags ctxt (c, [pos])));
 
 val type_alias =
   gen_alias Local_Theory.type_alias (K (K (fn c => (c, []))));
isabelle