# HG changeset patch
# User wenzelm
# Date 1737107610 -3600
# Node ID 834024a7863da1879330332652f13f9d1ef33797
# Parent  cc24add5b7386eee8d3a488ea47eb742250c05ab
clarified make_type: proper make_name;

diff -r cc24add5b738 -r 834024a7863d src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Fri Jan 17 10:51:47 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Fri Jan 17 10:53:30 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 c))
+      | NONE => Sign.full_name thy (Binding.name (make_name c)))
   in Type (d, args) end
 
 fun make_const thy (c, ty) =