match_bvs no longer puts a name in the alist if it is null ("")
authorlcp
Tue Jul 25 17:03:59 1995 +0200 (1995-07-25 ago)
changeset 1195686e3eb613b9
parent 1194 563ecd14c1d8
child 1196 d43c1f7a53fe
match_bvs no longer puts a name in the alist if it is null ("")
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Tue Jul 25 17:03:16 1995 +0200
     1.2 +++ b/src/Pure/thm.ML	Tue Jul 25 17:03:59 1995 +0200
     1.3 @@ -861,7 +861,9 @@
     1.4  
     1.5  (*Scan a pair of terms; while they are similar,
     1.6    accumulate corresponding bound vars in "al"*)
     1.7 -fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = match_bvs(s,t,(x,y)::al)
     1.8 +fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = 
     1.9 +      match_bvs(s, t, if x="" orelse y="" then al
    1.10 +		                          else (x,y)::al)
    1.11    | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
    1.12    | match_bvs(_,_,al) = al;
    1.13