# HG changeset patch
# User wenzelm
# Date 1737107770 -3600
# Node ID ea0c7189b15b56e6f76fe4bfba67180d85766aad
# Parent  834024a7863da1879330332652f13f9d1ef33797
tuned;

diff -r 834024a7863d -r ea0c7189b15b src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Fri Jan 17 10:53:30 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Fri Jan 17 10:56:10 2025 +0100
@@ -302,7 +302,7 @@
     val d =
       (case Import_Data.get_typ_map thy c of
         SOME d => d
-      | NONE => Sign.full_name thy (Binding.name (make_name c)))
+      | NONE => Sign.full_bname thy (make_name c))
   in Type (d, args) end
 
 fun make_const thy (c, ty) =
@@ -310,7 +310,7 @@
     val d =
       (case Import_Data.get_const_map thy c of
         SOME d => d
-      | NONE => Sign.full_name thy (Binding.name (make_name c)))
+      | NONE => Sign.full_bname thy (make_name c))
   in Const (d, ty) end
 
 fun get (map, no) s =