diff -r 348aed032cda -r 36ffe23b25f8 src/HOL/HOLCF/ex/Pattern_Match.thy
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Sat May 25 15:00:53 2013 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Sat May 25 15:37:53 2013 +0200
@@ -131,7 +131,7 @@
 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})];
 *}
 
@@ -164,7 +164,7 @@
               (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