diff -r 348aed032cda -r 36ffe23b25f8 src/Sequents/Modal0.thy
--- a/src/Sequents/Modal0.thy	Sat May 25 15:00:53 2013 +0200
+++ b/src/Sequents/Modal0.thy	Sat May 25 15:37:53 2013 +0200
@@ -27,13 +27,13 @@
 *}
 
 parse_translation {*
- [(@{syntax_const "_Lstar"}, star_tr @{const_syntax Lstar}),
-  (@{syntax_const "_Rstar"}, star_tr @{const_syntax Rstar})]
+ [(@{syntax_const "_Lstar"}, K (star_tr @{const_syntax Lstar})),
+  (@{syntax_const "_Rstar"}, K (star_tr @{const_syntax Rstar}))]
 *}
 
 print_translation {*
- [(@{const_syntax Lstar}, star_tr' @{syntax_const "_Lstar"}),
-  (@{const_syntax Rstar}, star_tr' @{syntax_const "_Rstar"})]
+ [(@{const_syntax Lstar}, K (star_tr' @{syntax_const "_Lstar"})),
+  (@{const_syntax Rstar}, K (star_tr' @{syntax_const "_Rstar"}))]
 *}
 
 defs