--- a/src/Pure/thm.ML Sun Aug 16 19:44:21 2015 +0200
+++ b/src/Pure/thm.ML Sun Aug 16 20:25:12 2015 +0200
@@ -40,6 +40,7 @@
val dest_fun2: cterm -> cterm
val dest_arg1: cterm -> cterm
val dest_abs: string option -> cterm -> cterm * cterm
+ val var: indexname * ctyp -> cterm
val apply: cterm -> cterm -> cterm
val lambda_name: string * cterm -> cterm -> cterm
val lambda: cterm -> cterm -> cterm
@@ -254,6 +255,10 @@
(* constructors *)
+fun var ((x, i), Ctyp {thy, T, maxidx, sorts}) =
+ if i < 0 then raise TERM ("var: bad index", [Var ((x, i), T)])
+ else Cterm {thy = thy, t = Var ((x, i), T), T = T, maxidx = Int.max (i, maxidx), sorts = sorts};
+
fun apply
(cf as Cterm {t = f, T = Type ("fun", [dty, rty]), maxidx = maxidx1, sorts = sorts1, ...})
(cx as Cterm {t = x, T, maxidx = maxidx2, sorts = sorts2, ...}) =