# HG changeset patch
# User lcp
# Date 806684639 -7200
# Node ID 686e3eb613b9ad677c6ad1709ad3b41c075ff0b4
# Parent  563ecd14c1d8600443c61203452fa401a18fbd20
match_bvs no longer puts a name in the alist if it is null ("")

diff -r 563ecd14c1d8 -r 686e3eb613b9 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Jul 25 17:03:16 1995 +0200
+++ b/src/Pure/thm.ML	Tue Jul 25 17:03:59 1995 +0200
@@ -861,7 +861,9 @@
 
 (*Scan a pair of terms; while they are similar,
   accumulate corresponding bound vars in "al"*)
-fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = match_bvs(s,t,(x,y)::al)
+fun match_bvs(Abs(x,_,s),Abs(y,_,t), al) = 
+      match_bvs(s, t, if x="" orelse y="" then al
+		                          else (x,y)::al)
   | match_bvs(f$s, g$t, al) = match_bvs(f,g,match_bvs(s,t,al))
   | match_bvs(_,_,al) = al;