--- 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