# HG changeset patch
# User wenzelm
# Date 1704883141 -3600
# Node ID fbdffff89f99229fba6035b3f76e43f491678ba8
# Parent  5f49d9d1bb195e71bb42ba4cbef4c4c7f1542a9e
clarified signature: more direct operations;

diff -r 5f49d9d1bb19 -r fbdffff89f99 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Wed Jan 10 11:33:36 2024 +0100
+++ b/src/Pure/consts.ML	Wed Jan 10 11:39:01 2024 +0100
@@ -16,6 +16,7 @@
    {const_space: Name_Space.T,
     constants: (string * (typ * term option)) list,
     constraints: (string * typ) list}
+  val get_const_name: T -> string -> string option
   val the_const: T -> string -> string * typ                   (*exception TYPE*)
   val the_abbreviation: T -> string -> typ * term              (*exception TYPE*)
   val type_scheme: T -> string -> typ                          (*exception TYPE*)
@@ -108,6 +109,9 @@
 
 (* lookup consts *)
 
+fun get_const_name (Consts {decls, ...}) c =
+  Name_Space.lookup_key decls c |> Option.map #1;
+
 fun the_entry (Consts {decls, ...}) c =
   (case Name_Space.lookup_key decls c of
     SOME entry => entry
diff -r 5f49d9d1bb19 -r fbdffff89f99 src/Pure/term_sharing.ML
--- a/src/Pure/term_sharing.ML	Wed Jan 10 11:33:36 2024 +0100
+++ b/src/Pure/term_sharing.ML	Wed Jan 10 11:39:01 2024 +0100
@@ -23,7 +23,7 @@
 
     val class = perhaps (try (#1 o Graph.get_entry (Sorts.classes_of algebra)));
     val tycon = perhaps (Option.map #1 o Name_Space.lookup_key types);
-    val const = perhaps (try (#1 o Consts.the_const (Sign.consts_of thy)));
+    val const = perhaps (Consts.get_const_name (Sign.consts_of thy));
 
     val typs = Unsynchronized.ref (Typtab.empty: Typtab.set);
     val terms = Unsynchronized.ref (Syntax_Termtab.empty: Syntax_Termtab.set);