# HG changeset patch
# User wenzelm
# Date 1737107507 -3600
# Node ID cc24add5b7386eee8d3a488ea47eb742250c05ab
# Parent  e6836cc115b9e8aaa15dde1fefc165a8677616fe
tuned;

diff -r e6836cc115b9 -r cc24add5b738 src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Fri Jan 17 10:46:59 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Fri Jan 17 10:51:47 2025 +0100
@@ -297,6 +297,14 @@
   let val b = "'" ^ String.translate (fn #"?" => "t" | c => Char.toString c) a
   in TFree (b, \<^sort>\<open>type\<close>) end
 
+fun make_type thy (c, args) =
+  let
+    val d =
+      (case Import_Data.get_typ_map thy c of
+        SOME d => d
+      | NONE => Sign.full_name thy (Binding.name c))
+  in Type (d, args) end
+
 fun make_const thy (c, ty) =
   let
     val d =
@@ -305,11 +313,6 @@
       | NONE => Sign.full_name thy (Binding.name (make_name c)))
   in Const (d, ty) end
 
-fun gettyname thy s =
-  case Import_Data.get_typ_map thy s of
-    SOME s => s
-  | NONE => Sign.full_name thy (Binding.name s)
-
 fun get (map, no) s =
   case Int.fromString s of
     NONE => error "Import_Rule.get: not a number"
@@ -425,7 +428,7 @@
           setty (Thm.global_ctyp_of thy (make_tfree n)) (thy, state)
       | process (thy, state) (#"a", n :: l) =
           fold_map getty l (thy, state) |>>
-            (fn tys => Thm.global_ctyp_of thy (Type (gettyname thy n, map Thm.typ_of tys))) |-> setty
+            (fn tys => Thm.global_ctyp_of thy (make_type thy (n, map Thm.typ_of tys))) |-> setty
       | process (thy, state) (#"v", [n, ty]) =
           getty ty (thy, state) |>> (fn ty => Thm.global_cterm_of thy (make_free (n, Thm.typ_of ty))) |-> settm
       | process (thy, state) (#"c", [n, ty]) =