diff -r 348aed032cda -r 36ffe23b25f8 src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Sat May 25 15:00:53 2013 +0200
+++ b/src/Sequents/LK0.thy	Sat May 25 15:37:53 2013 +0200
@@ -34,8 +34,8 @@
 syntax
  "_Trueprop"    :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
 
-parse_translation {* [(@{syntax_const "_Trueprop"}, two_seq_tr @{const_syntax Trueprop})] *}
-print_translation {* [(@{const_syntax Trueprop}, two_seq_tr' @{syntax_const "_Trueprop"})] *}
+parse_translation {* [(@{syntax_const "_Trueprop"}, K (two_seq_tr @{const_syntax Trueprop}))] *}
+print_translation {* [(@{const_syntax Trueprop}, K (two_seq_tr' @{syntax_const "_Trueprop"}))] *}
 
 abbreviation
   not_equal  (infixl "~=" 50) where