src/CCL/Term.thy
changeset 52143 36ffe23b25f8
parent 52037 837211662fb8
child 56199 8e8d28ed7529
--- a/src/CCL/Term.thy	Sat May 25 15:00:53 2013 +0200
+++ b/src/CCL/Term.thy	Sat May 25 15:37:53 2013 +0200
@@ -95,17 +95,17 @@
 *}
 
 parse_translation {*
- [(@{syntax_const "_let"}, let_tr),
-  (@{syntax_const "_letrec"}, letrec_tr),
-  (@{syntax_const "_letrec2"}, letrec2_tr),
-  (@{syntax_const "_letrec3"}, letrec3_tr)]
+ [(@{syntax_const "_let"}, K let_tr),
+  (@{syntax_const "_letrec"}, K letrec_tr),
+  (@{syntax_const "_letrec2"}, K letrec2_tr),
+  (@{syntax_const "_letrec3"}, K letrec3_tr)]
 *}
 
 print_translation {*
- [(@{const_syntax let}, let_tr'),
-  (@{const_syntax letrec}, letrec_tr'),
-  (@{const_syntax letrec2}, letrec2_tr'),
-  (@{const_syntax letrec3}, letrec3_tr')]
+ [(@{const_syntax let}, K let_tr'),
+  (@{const_syntax letrec}, K letrec_tr'),
+  (@{const_syntax letrec2}, K letrec2_tr'),
+  (@{const_syntax letrec3}, K letrec3_tr')]
 *}
 
 consts