# HG changeset patch
# User wenzelm
# Date 1704889008 -3600
# Node ID 4f862ca9a60a3dcf3ac5715efb26d56490e37b9b
# Parent  70bd3c59072860d59bdb514a92f4535f960f127d
tuned;

diff -r 70bd3c590728 -r 4f862ca9a60a src/Pure/consts.ML
--- a/src/Pure/consts.ML	Wed Jan 10 13:15:28 2024 +0100
+++ b/src/Pure/consts.ML	Wed Jan 10 13:16:48 2024 +0100
@@ -109,8 +109,7 @@
 
 (* lookup consts *)
 
-fun get_const_name (Consts {decls, ...}) c =
-  Name_Space.lookup_key decls c |> Option.map #1;
+fun get_const_name (Consts {decls, ...}) = Name_Space.lookup_key decls #> Option.map #1;
 
 fun get_entry (Consts {decls, ...}) = Name_Space.lookup decls;