src/HOL/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.(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 then g Int Compl({x}) else g Un {x})"
   srange_def