859 |
859 |
860 (*** Preservation of bound variable names ***) |
860 (*** Preservation of bound variable names ***) |
861 |
861 |
862 (*Scan a pair of terms; while they are similar, |
862 (*Scan a pair of terms; while they are similar, |
863 accumulate corresponding bound vars in "al"*) |
863 accumulate corresponding bound vars in "al"*) |
864 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = match_bvs(s,t,(x,y)::al) |
864 fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = |
|
865 match_bvs(s, t, if x="" orelse y="" then al |
|
866 else (x,y)::al) |
865 | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) |
867 | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al)) |
866 | match_bvs(_,_,al) = al; |
868 | match_bvs(_,_,al) = al; |
867 |
869 |
868 (* strip abstractions created by parameters *) |
870 (* strip abstractions created by parameters *) |
869 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al); |
871 fun match_bvars((s,t),al) = match_bvs(strip_abs_body s, strip_abs_body t, al); |