# 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;