--- a/src/Cube/Cube.thy Fri Jan 04 21:49:06 2019 +0100
+++ b/src/Cube/Cube.thy Fri Jan 04 23:22:53 2019 +0100
@@ -49,8 +49,8 @@
"\<Prod>x:A. B" \<rightharpoonup> "CONST Prod(A, \<lambda>x. B)"
"A \<rightarrow> B" \<rightharpoonup> "CONST Prod(A, \<lambda>_. B)"
print_translation \<open>
- [(@{const_syntax Prod},
- fn _ => Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))]
+ [(\<^const_syntax>\<open>Prod\<close>,
+ fn _ => Syntax_Trans.dependent_tr' (\<^syntax_const>\<open>_Pi\<close>, \<^syntax_const>\<open>_arrow\<close>))]
\<close>
axiomatization where