1.1 --- a/src/Cube/Cube.thy	Sun May 18 17:03:16 2008 +0200
     1.2 +++ b/src/Cube/Cube.thy	Mon Feb 08 21:28:27 2010 +0100
     1.3 @@ -43,9 +43,9 @@
     1.4  
     1.5  translations
     1.6    ("prop") "x:X" == ("prop") "|- x:X"
     1.7 -  "Lam x:A. B"   == "Abs(A, %x. B)"
     1.8 -  "Pi x:A. B"    => "Prod(A, %x. B)"
     1.9 -  "A -> B"       => "Prod(A, %_. B)"
    1.10 +  "Lam x:A. B"   == "CONST Abs(A, %x. B)"
    1.11 +  "Pi x:A. B"    => "CONST Prod(A, %x. B)"
    1.12 +  "A -> B"       => "CONST Prod(A, %_. B)"
    1.13  
    1.14  syntax (xsymbols)
    1.15    Trueprop      :: "[context', typing'] => prop"        ("(_/ \<turnstile> _)")
    1.16 @@ -54,7 +54,7 @@
    1.17    Pi            :: "[idt, term, term] => term"          ("(3\<Pi> _:_./ _)" [0, 0] 10)
    1.18    arrow         :: "[term, term] => term"               (infixr "\<rightarrow>" 10)
    1.19  
    1.20 -print_translation {* [("Prod", dependent_tr' ("Pi", "arrow"))] *}
    1.21 +print_translation {* [(@{const_syntax Prod}, dependent_tr' ("Pi", "arrow"))] *}
    1.22  
    1.23  axioms
    1.24    s_b:          "*: []"