clarified signature: more direct operations;

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

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