diff -r ab94035ba6ea -r 1a52baa70aed src/HOL/HOLCF/ex/Pattern_Match.thy
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Wed Oct 31 15:50:45 2018 +0100
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Wed Oct 31 15:53:32 2018 +0100
@@ -132,7 +132,7 @@
 (* rewrite (_pat x) => (succeed) *)
 (* rewrite (_variable x t) => (Abs_cfun (%x. t)) *)
  [(@{syntax_const "_pat"}, fn _ => fn _ => Syntax.const @{const_syntax Fixrec.succeed}),
-  Syntax_Trans.mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})];
+  Syntax_Trans.mk_binder_tr (@{syntax_const "_variable"}, @{const_syntax Abs_cfun})]
 \<close>
 
 text \<open>Printing Case expressions\<close>
@@ -164,7 +164,7 @@
               (Syntax.const @{syntax_const "_match"} $ p $ v) $ t
           end;
 
-  in [(@{const_syntax Rep_cfun}, K Case1_tr')] end;
+  in [(@{const_syntax Rep_cfun}, K Case1_tr')] end
 \<close>
 
 translations