src/Sequents/ILL.thy
changeset 52143 36ffe23b25f8
parent 51309 473303ef6e34
child 55228 901a6696cdd8
--- a/src/Sequents/ILL.thy	Sat May 25 15:00:53 2013 +0200
+++ b/src/Sequents/ILL.thy	Sat May 25 15:37:53 2013 +0200
@@ -36,15 +36,15 @@
   "_PromAux"  :: "three_seqe" ("promaux {_||_||_}")
 
 parse_translation {*
-  [(@{syntax_const "_Trueprop"}, single_tr @{const_syntax Trueprop}),
-   (@{syntax_const "_Context"}, two_seq_tr @{const_syntax Context}),
-   (@{syntax_const "_PromAux"}, three_seq_tr @{const_syntax PromAux})]
+  [(@{syntax_const "_Trueprop"}, K (single_tr @{const_syntax Trueprop})),
+   (@{syntax_const "_Context"}, K (two_seq_tr @{const_syntax Context})),
+   (@{syntax_const "_PromAux"}, K (three_seq_tr @{const_syntax PromAux}))]
 *}
 
 print_translation {*
-  [(@{const_syntax Trueprop}, single_tr' @{syntax_const "_Trueprop"}),
-   (@{const_syntax Context}, two_seq_tr' @{syntax_const "_Context"}),
-   (@{const_syntax PromAux}, three_seq_tr' @{syntax_const "_PromAux"})]
+  [(@{const_syntax Trueprop}, K (single_tr' @{syntax_const "_Trueprop"})),
+   (@{const_syntax Context}, K (two_seq_tr' @{syntax_const "_Context"})),
+   (@{const_syntax PromAux}, K (three_seq_tr' @{syntax_const "_PromAux"}))]
 *}
 
 defs