src/Cube/Cube.thy
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