Subst/Subst.thy

   subst_def    
   "t <| al == uterm_rec(t, %x.assoc(x,Var(x),al),	\
 \                          %x.Const(x),			\
 \                          %u v q r.Comb(q,r))"
 
-  comp_def     "al <> bl == alist_rec(al,bl,%x y xs g.Cons(<x,y <| bl>,g))"
+  comp_def     "al <> bl == alist_rec(al,bl,%x y xs g.<x,y <| bl>#g)"
 
   sdom_def
   "sdom(al) == alist_rec(al, {},  \
 \                        %x y xs g.if(Var(x)=y, g Int Compl({x}), g Un {x}))"
   srange_def