changeset 42284 | 326f57825e1a |
parent 41526 | 54b4686704af |
child 45241 | 87950f752099 |
--- a/src/Cube/Cube.thy Fri Apr 08 11:39:45 2011 +0200 +++ b/src/Cube/Cube.thy Fri Apr 08 13:31:16 2011 +0200 @@ -53,7 +53,8 @@ "_arrow" :: "[term, term] => term" (infixr "\<rightarrow>" 10) print_translation {* - [(@{const_syntax Prod}, dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))] + [(@{const_syntax Prod}, + Syntax_Trans.dependent_tr' (@{syntax_const "_Pi"}, @{syntax_const "_arrow"}))] *} axioms