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