# HG changeset patch
# User wenzelm
# Date 1737121645 -3600
# Node ID a001d14f150cea84e1219f3949f1cf56c5aef21a
# Parent  2a5cbd329241c51950a77f0896bb83f654cc4097
more direct Thm.free: avoid re-certification;

diff -r 2a5cbd329241 -r a001d14f150c src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Fri Jan 17 14:31:48 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Fri Jan 17 14:47:25 2025 +0100
@@ -198,9 +198,7 @@
     val P = Thm.dest_arg cn
     val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept)
   in
-    typedef_hol2hollight nty oty rept abst P
-      (Thm.global_cterm_of thy (Free ("a", Thm.typ_of nty)))
-      (Thm.global_cterm_of thy (Free ("r", Thm.typ_of oty)))
+    typedef_hol2hollight nty oty rept abst P (Thm.free ("a", nty)) (Thm.free ("r", oty))
   end
 
 fun tydef' tycname abs_name rep_name cP ct td_th thy =
@@ -224,19 +222,16 @@
      (Typedef.add_typedef {overloaded = false}
        (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
        (SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1)) thy
-    val aty = #abs_type (#1 typedef_info)
+    val aty = Thm.global_ctyp_of thy' (#abs_type (#1 typedef_info))
     val th = freezeT thy' (#type_definition (#2 typedef_info))
     val (th_s, _) = Thm.dest_comb (Thm.dest_arg (Thm.cprop_of th))
     val (th_s, abst) = Thm.dest_comb th_s
     val rept = Thm.dest_arg th_s
     val [nty, oty] = Thm.dest_ctyp (Thm.ctyp_of_cterm rept)
     val typedef_th =
-      typedef_hol2hollight nty oty rept abst cP
-        (Thm.global_cterm_of thy' (Free ("a", aty)))
-        (Thm.global_cterm_of thy' (Free ("r", Thm.typ_of ctT)))
-    val th4 = typedef_th OF [#type_definition (#2 typedef_info)]
+      typedef_hol2hollight nty oty rept abst cP (Thm.free ("a", aty)) (Thm.free ("r", ctT))
   in
-    (th4, thy')
+    (typedef_th OF [#type_definition (#2 typedef_info)], thy')
   end
 
 fun mtydef thy name =
diff -r 2a5cbd329241 -r a001d14f150c src/Pure/thm.ML
--- a/src/Pure/thm.ML	Fri Jan 17 14:31:48 2025 +0100
+++ b/src/Pure/thm.ML	Fri Jan 17 14:47:25 2025 +0100
@@ -49,6 +49,7 @@
   val dest_abs_fresh: string -> cterm -> cterm * cterm
   val dest_abs_global: cterm -> cterm * cterm
   val rename_tvar: indexname -> ctyp -> ctyp
+  val free: string * ctyp -> cterm
   val var: indexname * ctyp -> cterm
   val apply: cterm -> cterm -> cterm
   val lambda_name: string * cterm -> cterm -> cterm
@@ -340,6 +341,9 @@
     val _ = if i < 0 then raise TYPE ("rename_tvar: bad index", [TVar ((a, i), S)], []) else ();
   in Ctyp {cert = cert, T = TVar ((a, i), S), maxidx = Int.max (i, maxidx), sorts = sorts} end;
 
+fun free (x, Ctyp {cert, T, maxidx, sorts}) =
+  Cterm {cert = cert, t = Free (x, T), T = T, maxidx = maxidx, sorts = sorts};
+
 fun var ((x, i), Ctyp {cert, T, maxidx, sorts}) =
   if i < 0 then raise TERM ("var: bad index", [Var ((x, i), T)])
   else Cterm {cert = cert, t = Var ((x, i), T), T = T, maxidx = Int.max (i, maxidx), sorts = sorts};