src/HOL/HOLCF/ex/Pattern_Match.thy

   "_variable _noargs r" => "CONST unit_when\<cdot>r"
 
 parse_translation {*
 (* rewrite (_pat x) => (succeed) *)
 (* rewrite (_variable x t) => (Abs_cfun (%x. t)) *)
- [(@{syntax_const "_pat"}, fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
+ [(@{syntax_const "_pat"}, fn _ => fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
   Syntax_Trans.mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})];
 *}
 
 text {* Printing Case expressions *}
 

           let val (v, t) = dest_LAM r in
             Syntax.const @{syntax_const "_Case1"} $
               (Syntax.const @{syntax_const "_match"} $ p $ v) $ t
           end;
 
-  in [(@{const_syntax Rep_cfun}, Case1_tr')] end;
+  in [(@{const_syntax Rep_cfun}, K Case1_tr')] end;
 *}
 
 translations
   "x" <= "_match (CONST succeed) (_variable x)"