--- a/src/Cube/Cube.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/Cube/Cube.thy Mon Feb 08 21:28:27 2010 +0100
@@ -43,9 +43,9 @@
translations
("prop") "x:X" == ("prop") "|- x:X"
- "Lam x:A. B" == "Abs(A, %x. B)"
- "Pi x:A. B" => "Prod(A, %x. B)"
- "A -> B" => "Prod(A, %_. B)"
+ "Lam x:A. B" == "CONST Abs(A, %x. B)"
+ "Pi x:A. B" => "CONST Prod(A, %x. B)"
+ "A -> B" => "CONST Prod(A, %_. B)"
syntax (xsymbols)
Trueprop :: "[context', typing'] => prop" ("(_/ \<turnstile> _)")
@@ -54,7 +54,7 @@
Pi :: "[idt, term, term] => term" ("(3\<Pi> _:_./ _)" [0, 0] 10)
arrow :: "[term, term] => term" (infixr "\<rightarrow>" 10)
-print_translation {* [("Prod", dependent_tr' ("Pi", "arrow"))] *}
+print_translation {* [(@{const_syntax Prod}, dependent_tr' ("Pi", "arrow"))] *}
axioms
s_b: "*: []"