0

1 
(* Title: term.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright Cambridge University 1992


5 
*)


6 


7 


8 
(*Simply typed lambdacalculus: types, terms, and basic operations*)


9 


10 


11 
(*Indexnames can be quickly renamed by adding an offset to the integer part,


12 
for resolution.*)


13 
type indexname = string*int;


14 


15 
(* Types are classified by classes. *)


16 
type class = string;


17 
type sort = class list;


18 


19 
(* The sorts attached to TFrees and TVars specify the sort of that variable *)


20 
datatype typ = Type of string * typ list


21 
 TFree of string * sort


22 
 TVar of indexname * sort;


23 


24 
infixr 5 >;


25 
fun S > T = Type("fun",[S,T]);


26 


27 
(*handy for multiple args: [T1,...,Tn]>T gives T1>(T2> ... >T)*)


28 
infixr >;


29 
val op > = foldr (op >);


30 


31 


32 
(*terms. Bound variables are indicated by depth number.


33 
Free variables, (scheme) variables and constants have names.


34 
An term is "closed" if there every bound variable of level "lev"


35 
is enclosed by at least "lev" abstractions.


36 


37 
It is possible to create meaningless terms containing loose bound vars


38 
or type mismatches. But such terms are not allowed in rules. *)


39 


40 


41 


42 
infix 9 $; (*application binds tightly!*)


43 
datatype term =


44 
Const of string * typ


45 
 Free of string * typ


46 
 Var of indexname * typ


47 
 Bound of int


48 
 Abs of string*typ*term


49 
 op $ of term*term;


50 


51 


52 
(*For errors involving type mismatches*)


53 
exception TYPE of string * typ list * term list;


54 


55 
(*For system errors involving terms*)


56 
exception TERM of string * term list;


57 


58 


59 
(*Note variable naming conventions!


60 
a,b,c: string


61 
f,g,h: functions (including terms of function type)


62 
i,j,m,n: int


63 
t,u: term


64 
v,w: indexnames


65 
x,y: any


66 
A,B,C: term (denoting formulae)


67 
T,U: typ


68 
*)


69 


70 


71 
(** Discriminators **)


72 


73 
fun is_Const (Const _) = true


74 
 is_Const _ = false;


75 


76 
fun is_Free (Free _) = true


77 
 is_Free _ = false;


78 


79 
fun is_Var (Var _) = true


80 
 is_Var _ = false;


81 


82 
fun is_TVar (TVar _) = true


83 
 is_TVar _ = false;


84 


85 
(** Destructors **)


86 


87 
fun dest_Const (Const x) = x


88 
 dest_Const t = raise TERM("dest_Const", [t]);


89 


90 
fun dest_Free (Free x) = x


91 
 dest_Free t = raise TERM("dest_Free", [t]);


92 


93 
fun dest_Var (Var x) = x


94 
 dest_Var t = raise TERM("dest_Var", [t]);


95 


96 


97 
(* maps [T1,...,Tn]>T to the list [T1,T2,...,Tn]*)


98 
fun binder_types (Type("fun",[S,T])) = S :: binder_types T


99 
 binder_types _ = [];


100 


101 
(* maps [T1,...,Tn]>T to T*)


102 
fun body_type (Type("fun",[S,T])) = body_type T


103 
 body_type T = T;


104 


105 
(* maps [T1,...,Tn]>T to ([T1,T2,...,Tn], T) *)


106 
fun strip_type T : typ list * typ =


107 
(binder_types T, body_type T);


108 


109 


110 
(*Compute the type of the term, checking that combinations are welltyped


111 
Ts = [T0,T1,...] holds types of bound variables 0, 1, ...*)


112 
fun type_of1 (Ts, Const (_,T)) = T


113 
 type_of1 (Ts, Free (_,T)) = T


114 
 type_of1 (Ts, Bound i) = (nth_elem (i,Ts)


115 
handle LIST _ => raise TYPE("type_of: bound variable", [], [Bound i]))


116 
 type_of1 (Ts, Var (_,T)) = T


117 
 type_of1 (Ts, Abs (_,T,body)) = T > type_of1(T::Ts, body)


118 
 type_of1 (Ts, f$u) =


119 
let val U = type_of1(Ts,u)


120 
and T = type_of1(Ts,f)


121 
in case T of


122 
Type("fun",[T1,T2]) =>


123 
if T1=U then T2 else raise TYPE


124 
("type_of: type mismatch in application", [T1,U], [f$u])


125 
 _ => raise TYPE ("type_of: Rator must have function type",


126 
[T,U], [f$u])


127 
end;


128 


129 


130 
fun type_of t : typ = type_of1 ([],t);


131 


132 
(*Determines the type of a term, with minimal checking*)


133 
fun fastype_of(Ts, f$u) = (case fastype_of(Ts,f) of


134 
Type("fun",[_,T]) => T


135 
 _ => raise TERM("fastype_of: expected function type", [f$u]))


136 
 fastype_of(_, Const (_,T)) = T


137 
 fastype_of(_, Free (_,T)) = T


138 
 fastype_of(Ts, Bound i) = (nth_elem(i,Ts)


139 
handle LIST _ => raise TERM("fastype_of: Bound", [Bound i]))


140 
 fastype_of(_, Var (_,T)) = T


141 
 fastype_of(Ts, Abs (_,T,u)) = T > fastype_of(T::Ts, u);


142 


143 


144 
(* maps (x1,...,xn)t to t *)


145 
fun strip_abs_body (Abs(_,_,t)) = strip_abs_body t


146 
 strip_abs_body u = u;


147 


148 


149 
(* maps (x1,...,xn)t to [x1, ..., xn] *)


150 
fun strip_abs_vars (Abs(a,T,t)) = (a,T) :: strip_abs_vars t


151 
 strip_abs_vars u = [] : (string*typ) list;


152 


153 


154 
fun strip_qnt_body qnt =


155 
let fun strip(tm as Const(c,_)$Abs(_,_,t)) = if c=qnt then strip t else tm


156 
 strip t = t


157 
in strip end;


158 


159 
fun strip_qnt_vars qnt =


160 
let fun strip(Const(c,_)$Abs(a,T,t)) = if c=qnt then (a,T)::strip t else []


161 
 strip t = [] : (string*typ) list


162 
in strip end;


163 


164 


165 
(* maps (f, [t1,...,tn]) to f(t1,...,tn) *)


166 
val list_comb : term * term list > term = foldl (op $);


167 


168 


169 
(* maps f(t1,...,tn) to (f, [t1,...,tn]) ; naturally tailrecursive*)


170 
fun strip_comb u : term * term list =


171 
let fun stripc (f$t, ts) = stripc (f, t::ts)


172 
 stripc x = x


173 
in stripc(u,[]) end;


174 


175 


176 
(* maps f(t1,...,tn) to f , which is never a combination *)


177 
fun head_of (f$t) = head_of f


178 
 head_of u = u;


179 


180 


181 
(*Number of atoms and abstractions in a term*)


182 
fun size_of_term (Abs (_,_,body)) = 1 + size_of_term body


183 
 size_of_term (f$t) = size_of_term f + size_of_term t


184 
 size_of_term _ = 1;


185 


186 


187 
(* apply a function to all types in a term *)


188 
fun map_term_types f =


189 
let fun map(Const(a,T)) = Const(a, f T)


190 
 map(Free(a,T)) = Free(a, f T)


191 
 map(Var(v,T)) = Var(v, f T)


192 
 map(t as Bound _) = t


193 
 map(Abs(a,T,t)) = Abs(a, f T, map t)


194 
 map(f$t) = map f $ map t;


195 
in map end;


196 


197 
(* iterate a function over all types in a term *)


198 
fun it_term_types f =


199 
let fun iter(Const(_,T), a) = f(T,a)


200 
 iter(Free(_,T), a) = f(T,a)


201 
 iter(Var(_,T), a) = f(T,a)


202 
 iter(Abs(_,T,t), a) = iter(t,f(T,a))


203 
 iter(f$u, a) = iter(f, iter(u, a))


204 
 iter(Bound _, a) = a


205 
in iter end


206 


207 


208 
(** Connectives of higher order logic **)


209 


210 
val propT : typ = Type("prop",[]);


211 


212 
val implies = Const("==>", propT>propT>propT);


213 


214 
fun all T = Const("all", (T>propT)>propT);


215 


216 
fun equals T = Const("==", T>T>propT);


217 


218 
fun flexpair T = Const("=?=", T>T>propT);


219 


220 
(* maps !!x1...xn. t to t *)


221 
fun strip_all_body (Const("all",_)$Abs(_,_,t)) = strip_all_body t


222 
 strip_all_body t = t;


223 


224 
(* maps !!x1...xn. t to [x1, ..., xn] *)


225 
fun strip_all_vars (Const("all",_)$Abs(a,T,t)) =


226 
(a,T) :: strip_all_vars t


227 
 strip_all_vars t = [] : (string*typ) list;


228 


229 
(*increments a term's nonlocal bound variables


230 
required when moving a term within abstractions


231 
inc is increment for bound variables


232 
lev is level at which a bound variable is considered 'loose'*)


233 
fun incr_bv (inc, lev, u as Bound i) = if i>=lev then Bound(i+inc) else u


234 
 incr_bv (inc, lev, Abs(a,T,body)) =


235 
Abs(a, T, incr_bv(inc,lev+1,body))


236 
 incr_bv (inc, lev, f$t) =


237 
incr_bv(inc,lev,f) $ incr_bv(inc,lev,t)


238 
 incr_bv (inc, lev, u) = u;


239 


240 
fun incr_boundvars 0 t = t


241 
 incr_boundvars inc t = incr_bv(inc,0,t);


242 


243 


244 
(*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.


245 
(Bound 0) is loose at level 0 *)


246 
fun add_loose_bnos (Bound i, lev, js) =


247 
if i<lev then js else (ilev) :: js


248 
 add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)


249 
 add_loose_bnos (f$t, lev, js) =


250 
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))


251 
 add_loose_bnos (_, _, js) = js;


252 


253 
fun loose_bnos t = add_loose_bnos (t, 0, []);


254 


255 
(* loose_bvar(t,k) iff t contains a 'loose' bound variable referring to


256 
level k or beyond. *)


257 
fun loose_bvar(Bound i,k) = i >= k


258 
 loose_bvar(f$t, k) = loose_bvar(f,k) orelse loose_bvar(t,k)


259 
 loose_bvar(Abs(_,_,t),k) = loose_bvar(t,k+1)


260 
 loose_bvar _ = false;


261 


262 


263 
(*Substitute arguments for loose bound variables.


264 
Betareduction of arg(n1)...arg0 into t replacing (Bound i) with (argi).


265 
Note that for ((x,y)c)(a,b), the bound vars in c are x=1 and y=0


266 
and the appropriate call is subst_bounds([b,a], c) .


267 
Loose bound variables >=n are reduced by "n" to


268 
compensate for the disappearance of lambdas.


269 
*)


270 
fun subst_bounds (args: term list, t) : term =


271 
let val n = length args;


272 
fun subst (t as Bound i, lev) =


273 
if i<lev then t (*var is locally bound*)


274 
else (case (drop (ilev,args)) of


275 
[] => Bound(in) (*loose: change it*)


276 
 arg::_ => incr_boundvars lev arg)


277 
 subst (Abs(a,T,body), lev) = Abs(a, T, subst(body,lev+1))


278 
 subst (f$t, lev) = subst(f,lev) $ subst(t,lev)


279 
 subst (t,lev) = t


280 
in case args of [] => t  _ => subst (t,0) end;


281 


282 
(*betareduce if possible, else form application*)


283 
fun betapply (Abs(_,_,t), u) = subst_bounds([u],t)


284 
 betapply (f,u) = f$u;


285 


286 
(*Tests whether 2 terms are alphaconvertible and have same type.


287 
Note that constants and Vars may have more than one type.*)


288 
infix aconv;


289 
fun (Const(a,T)) aconv (Const(b,U)) = a=b andalso T=U


290 
 (Free(a,T)) aconv (Free(b,U)) = a=b andalso T=U


291 
 (Var(v,T)) aconv (Var(w,U)) = v=w andalso T=U


292 
 (Bound i) aconv (Bound j) = i=j


293 
 (Abs(_,T,t)) aconv (Abs(_,U,u)) = t aconv u andalso T=U


294 
 (f$t) aconv (g$u) = (f aconv g) andalso (t aconv u)


295 
 _ aconv _ = false;


296 


297 
(*are two term lists alphaconvertible in corresponding elements?*)


298 
fun aconvs ([],[]) = true


299 
 aconvs (t::ts, u::us) = t aconv u andalso aconvs(ts,us)


300 
 aconvs _ = false;


301 


302 
(*A fast unification filter: true unless the two terms cannot be unified.


303 
Terms must be NORMAL. Treats all Vars as distinct. *)


304 
fun could_unify (t,u) =


305 
let fun matchrands (f$t, g$u) = could_unify(t,u) andalso matchrands(f,g)


306 
 matchrands _ = true


307 
in case (head_of t , head_of u) of


308 
(_, Var _) => true


309 
 (Var _, _) => true


310 
 (Const(a,_), Const(b,_)) => a=b andalso matchrands(t,u)


311 
 (Free(a,_), Free(b,_)) => a=b andalso matchrands(t,u)


312 
 (Bound i, Bound j) => i=j andalso matchrands(t,u)


313 
 (Abs _, _) => true (*because of possible eta equality*)


314 
 (_, Abs _) => true


315 
 _ => false


316 
end;


317 


318 
(*Substitute new for free occurrences of old in a term*)


319 
fun subst_free [] = (fn t=>t)


320 
 subst_free pairs =


321 
let fun substf u =


322 
case gen_assoc (op aconv) (pairs, u) of


323 
Some u' => u'


324 
 None => (case u of Abs(a,T,t) => Abs(a, T, substf t)


325 
 t$u' => substf t $ substf u'


326 
 _ => u)


327 
in substf end;


328 


329 
(*a total, irreflexive ordering on index names*)


330 
fun xless ((a,i), (b,j): indexname) = i<j orelse (i=j andalso a<b);


331 


332 


333 
(*Abstraction of the term "body" over its occurrences of v,


334 
which must contain no loose bound variables.


335 
The resulting term is ready to become the body of an Abs.*)


336 
fun abstract_over (v,body) =


337 
let fun abst (lev,u) = if (v aconv u) then (Bound lev) else


338 
(case u of


339 
Abs(a,T,t) => Abs(a, T, abst(lev+1, t))


340 
 f$rand => abst(lev,f) $ abst(lev,rand)


341 
 _ => u)


342 
in abst(0,body) end;


343 


344 


345 
(*Form an abstraction over a free variable.*)


346 
fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));


347 


348 
(*Abstraction over a list of free variables*)


349 
fun list_abs_free ([ ] , t) = t


350 
 list_abs_free ((a,T)::vars, t) =


351 
absfree(a, T, list_abs_free(vars,t));


352 


353 
(*Quantification over a list of free variables*)


354 
fun list_all_free ([], t: term) = t


355 
 list_all_free ((a,T)::vars, t) =


356 
(all T) $ (absfree(a, T, list_all_free(vars,t)));


357 


358 
(*Quantification over a list of variables (already bound in body) *)


359 
fun list_all ([], t) = t


360 
 list_all ((a,T)::vars, t) =


361 
(all T) $ (Abs(a, T, list_all(vars,t)));


362 


363 
(*Replace the ATOMIC term ti by ui; instl = [(t1,u1), ..., (tn,un)].


364 
A simultaneous substitution: [ (a,b), (b,a) ] swaps a and b. *)


365 
fun subst_atomic [] t = t : term


366 
 subst_atomic (instl: (term*term) list) t =


367 
let fun subst (Abs(a,T,body)) = Abs(a, T, subst body)


368 
 subst (f$t') = subst f $ subst t'


369 
 subst t = (case assoc(instl,t) of


370 
Some u => u  None => t)


371 
in subst t end;


372 


373 
fun typ_subst_TVars iTs T = if null iTs then T else


374 
let fun subst(Type(a,Ts)) = Type(a, map subst Ts)


375 
 subst(T as TFree _) = T


376 
 subst(T as TVar(ixn,_)) =


377 
(case assoc(iTs,ixn) of None => T  Some(U) => U)


378 
in subst T end;


379 


380 
val subst_TVars = map_term_types o typ_subst_TVars;


381 


382 
fun subst_Vars itms t = if null itms then t else


383 
let fun subst(v as Var(ixn,_)) =


384 
(case assoc(itms,ixn) of None => v  Some t => t)


385 
 subst(Abs(a,T,t)) = Abs(a,T,subst t)


386 
 subst(f$t) = subst f $ subst t


387 
 subst(t) = t


388 
in subst t end;


389 


390 
fun subst_vars(iTs,itms) = if null iTs then subst_Vars itms else


391 
let fun subst(Const(a,T)) = Const(a,typ_subst_TVars iTs T)


392 
 subst(Free(a,T)) = Free(a,typ_subst_TVars iTs T)


393 
 subst(v as Var(ixn,T)) = (case assoc(itms,ixn) of


394 
None => Var(ixn,typ_subst_TVars iTs T)


395 
 Some t => t)


396 
 subst(b as Bound _) = b


397 
 subst(Abs(a,T,t)) = Abs(a,typ_subst_TVars iTs T,subst t)


398 
 subst(f$t) = subst f $ subst t


399 
in subst end;


400 


401 


402 
(*Computing the maximum index of a typ*)


403 
fun maxidx_of_typ(Type(_,Ts)) =


404 
if Ts=[] then ~1 else max(map maxidx_of_typ Ts)


405 
 maxidx_of_typ(TFree _) = ~1


406 
 maxidx_of_typ(TVar((_,i),_)) = i;


407 


408 


409 
(*Computing the maximum index of a term*)


410 
fun maxidx_of_term (Const(_,T)) = maxidx_of_typ T


411 
 maxidx_of_term (Bound _) = ~1


412 
 maxidx_of_term (Free(_,T)) = maxidx_of_typ T


413 
 maxidx_of_term (Var ((_,i), T)) = max[i, maxidx_of_typ T]


414 
 maxidx_of_term (Abs (_,T,body)) = max[maxidx_of_term body, maxidx_of_typ T]


415 
 maxidx_of_term (f$t) = max [maxidx_of_term f, maxidx_of_term t];


416 


417 


418 
(* Increment the index of all Poly's in T by k *)


419 
fun incr_tvar k (Type(a,Ts)) = Type(a, map (incr_tvar k) Ts)


420 
 incr_tvar k (T as TFree _) = T


421 
 incr_tvar k (TVar((a,i),rs)) = TVar((a,i+k),rs);


422 


423 


424 
(**** Syntaxrelated declarations ****)


425 


426 


427 
(*Dummy type for parsing. Will be replaced during type inference. *)


428 
val dummyT = Type("dummy",[]);


429 


430 
(*scan a numeral of the given radix, normally 10*)


431 
fun scan_radixint (radix: int, cs) : int * string list =


432 
let val zero = ord"0"


433 
val limit = zero+radix


434 
fun scan (num,[]) = (num,[])


435 
 scan (num, c::cs) =


436 
if zero <= ord c andalso ord c < limit


437 
then scan(radix*num + ord c  zero, cs)


438 
else (num, c::cs)


439 
in scan(0,cs) end;


440 


441 
fun scan_int cs = scan_radixint(10,cs);


442 


443 


444 
(*** Printing ***)


445 


446 


447 
(*Makes a variant of the name c distinct from the names in bs.


448 
First attaches the suffix "a" and then increments this. *)


449 
fun variant bs c : string =


450 
let fun vary2 c = if (c mem bs) then vary2 (bump_string c) else c


451 
fun vary1 c = if (c mem bs) then vary2 (c ^ "a") else c


452 
in vary1 (if c="" then "u" else c) end;


453 


454 
(*Create variants of the list of names, with priority to the first ones*)


455 
fun variantlist ([], used) = []


456 
 variantlist(b::bs, used) =


457 
let val b' = variant used b


458 
in b' :: variantlist (bs, b'::used) end;


459 


460 
(** TFrees and TVars **)


461 


462 
(*maps (bs,v) to v'::bs this reverses the identifiers bs*)


463 
fun add_new_id (bs, c) : string list = variant bs c :: bs;


464 


465 
(*Accumulates the names in the term, suppressing duplicates.


466 
Includes Frees and Consts. For choosing unambiguous bound var names.*)


467 
fun add_term_names (Const(a,_), bs) = a ins bs


468 
 add_term_names (Free(a,_), bs) = a ins bs


469 
 add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))


470 
 add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)


471 
 add_term_names (_, bs) = bs;


472 


473 
(*Accumulates the TVars in a type, suppressing duplicates. *)


474 
fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars (Ts,vs)


475 
 add_typ_tvars(TFree(_),vs) = vs


476 
 add_typ_tvars(TVar(v),vs) = v ins vs;


477 


478 
(*Accumulates the TFrees in a type, suppressing duplicates. *)


479 
fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names (Ts,fs)


480 
 add_typ_tfree_names(TFree(f,_),fs) = f ins fs


481 
 add_typ_tfree_names(TVar(_),fs) = fs;


482 


483 
fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees (Ts,fs)


484 
 add_typ_tfrees(TFree(f),fs) = f ins fs


485 
 add_typ_tfrees(TVar(_),fs) = fs;


486 


487 
(*Accumulates the TVars in a term, suppressing duplicates. *)


488 
val add_term_tvars = it_term_types add_typ_tvars;


489 
val add_term_tvar_ixns = (map #1) o (it_term_types add_typ_tvars);


490 


491 
(*Accumulates the TFrees in a term, suppressing duplicates. *)


492 
val add_term_tfrees = it_term_types add_typ_tfrees;


493 
val add_term_tfree_names = it_term_types add_typ_tfree_names;


494 


495 
(*Nonlist versions*)


496 
fun typ_tfrees T = add_typ_tfrees(T,[]);


497 
fun typ_tvars T = add_typ_tvars(T,[]);


498 
fun term_tfrees t = add_term_tfrees(t,[]);


499 
fun term_tvars t = add_term_tvars(t,[]);


500 


501 
(** Frees and Vars **)


502 


503 
(*a partial ordering (not reflexive) for atomic terms*)


504 
fun atless (Const (a,_), Const (b,_)) = a<b


505 
 atless (Free (a,_), Free (b,_)) = a<b


506 
 atless (Var(v,_), Var(w,_)) = xless(v,w)


507 
 atless (Bound i, Bound j) = i<j


508 
 atless _ = false;


509 


510 
(*insert atomic term into partially sorted list, suppressing duplicates (?)*)


511 
fun insert_aterm (t,us) =


512 
let fun inserta [] = [t]


513 
 inserta (us as u::us') =


514 
if atless(t,u) then t::us


515 
else if t=u then us (*duplicate*)


516 
else u :: inserta(us')


517 
in inserta us end;


518 


519 
(*Accumulates the Vars in the term, suppressing duplicates*)


520 
fun add_term_vars (t, vars: term list) = case t of


521 
Var _ => insert_aterm(t,vars)


522 
 Abs (_,_,body) => add_term_vars(body,vars)


523 
 f$t => add_term_vars (f, add_term_vars(t, vars))


524 
 _ => vars;


525 


526 
fun term_vars t = add_term_vars(t,[]);


527 


528 
(*Accumulates the Frees in the term, suppressing duplicates*)


529 
fun add_term_frees (t, frees: term list) = case t of


530 
Free _ => insert_aterm(t,frees)


531 
 Abs (_,_,body) => add_term_frees(body,frees)


532 
 f$t => add_term_frees (f, add_term_frees(t, frees))


533 
 _ => frees;


534 


535 
fun term_frees t = add_term_frees(t,[]);


536 


537 
(*Given an abstraction over P, replaces the bound variable by a Free variable


538 
having a unique name. *)


539 
fun variant_abs (a,T,P) =


540 
let val b = variant (add_term_names(P,[])) a


541 
in (b, subst_bounds ([Free(b,T)], P)) end;


542 


543 
(* renames and reverses the strings in vars away from names *)


544 
fun rename_aTs names vars : (string*typ)list =


545 
let fun rename_aT (vars,(a,T)) =


546 
(variant (map #1 vars @ names) a, T) :: vars


547 
in foldl rename_aT ([],vars) end;


548 


549 
fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
