src/CCL/ex/flag.thy

   ccase_def   "ccase(c,r,w,b) == when(c,%x.r,%wb.when(wb,%x.w,%x.b))"
 
   flag_def    "flag == lam l.letrec \
 \      flagx l be lcase(l,<[],<[],[]>>, \
 \                       %h t. split(flagx(t),%lr p.split(p,%lw lb. \
-\                            ccase(h, <red.lr,<lw,lb>>, \
-\                                     <lr,<white.lw,lb>>, \
-\                                     <lr,<lw,blue.lb>>)))) \
+\                            ccase(h, <red$lr,<lw,lb>>, \
+\                                     <lr,<white$lw,lb>>, \
+\                                     <lr,<lw,blue$lb>>)))) \
 \      in flagx(l)"    
 
   Flag_def
      "Flag(l,x) == ALL lr:List(Colour).ALL lw:List(Colour).ALL lb:List(Colour). \
 \                    x = <lr,<lw,lb>> --> \