--- a/src/CCL/Type.thy Sat May 25 15:00:53 2013 +0200
+++ b/src/CCL/Type.thy Sat May 25 15:37:53 2013 +0200
@@ -47,9 +47,9 @@
print_translation {*
[(@{const_syntax Pi},
- Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
+ fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"})),
(@{const_syntax Sigma},
- Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
+ fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Sigma"}, @{syntax_const "_star"}))]
*}
defs