--- 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]) =