--- 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};