*** opensem.str.~1~	2006-04-07 13:58:29.000000000 +0200
--- opensem.str	2006-08-19 19:20:29.000000000 +0200
***************
*** 680,686 ****
  				val Q' = if np = 0 then Q''
  					 else B.beta_reduce Q'' (nns,0)
  				val f =
! 				    Lib.del_dups N.eq ((Lib.filter (fn x=> not(Lib.member N.eq (x,nns))) vp)@(Lib.filter (fn x=> not(Lib.member N.eq (x,nns))) vq)@(B.free_names P')@(B.free_names Q'))
  				val C' = 
  				    Lib.fold (fn (nn,c)=>
  					  Lib.fold (fn (f,c)=>
--- 680,688 ----
  				val Q' = if np = 0 then Q''
  					 else B.beta_reduce Q'' (nns,0)
  				val f =
! (*  				    Lib.del_dups N.eq (vp@vq@(B.free_names P')@(B.free_names Q')) *)
!     (* BV 060819: make new names distinct from all OTHER free names *)
! 				    Lib.del_dups N.eq (Lib.filter (fn x=> not(Lib.member N.eq (x,nns))) (vp@vq@(B.free_names P')@(B.free_names Q')))
  				val C' = 
  				    Lib.fold (fn (nn,c)=>
  					  Lib.fold (fn (f,c)=>

