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/HOLCF/ex/Pattern_Match.thy
changeset 80636 4041e7c8059d
parent 80634 a90ab1ea6458
child 80661 231d58c412b5 
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Aug 04 16:56:28 2024 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Sun Aug 04 17:39:47 2024 +0200
@@ -494,7 +494,7 @@
 
     (* syntax translations for pattern combinators *)
     local
-      fun syntax c = Lexicon.mark_const (fst (dest_Const c));
+      fun syntax c = Lexicon.mark_const (dest_Const_name c);
       fun app s (l, r) = Ast.mk_appl (Ast.Constant s) [l, r];
       val capp = app \<^const_syntax>\<open>Rep_cfun\<close>;
       val capps = Library.foldl capp
isabelle