src/Pure/thm.ML

   val dest_fun: cterm -> cterm
   val dest_arg: cterm -> cterm
   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
   val adjust_maxidx_cterm: int -> cterm -> cterm
   val incr_indexes_cterm: int -> cterm -> cterm

   | dest_abs _ ct = raise CTERM ("dest_abs", [ct]);
 
 
 (* 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, ...}) =
     if T = dty then
       Cterm {thy = merge_thys0 cf cx,