src/Sequents/Sequents.thy
changeset 52143 36ffe23b25f8
parent 48891 c0eafbd55de3
child 55228 901a6696cdd8
--- a/src/Sequents/Sequents.thy	Sat May 25 15:00:53 2013 +0200
+++ b/src/Sequents/Sequents.thy	Sat May 25 15:37:53 2013 +0200
@@ -139,7 +139,7 @@
 fun side_tr [s1] = seq_tr s1;
 *}
 
-parse_translation {* [(@{syntax_const "_Side"}, side_tr)] *}
+parse_translation {* [(@{syntax_const "_Side"}, K side_tr)] *}
 
 ML_file "prover.ML"