1.1 --- a/src/CCL/Type.thy	Thu Jul 23 21:59:56 2009 +0200
     1.2 +++ b/src/CCL/Type.thy	Mon Feb 08 21:28:27 2010 +0100
     1.3 @@ -39,15 +39,15 @@
     1.4    "@Subtype"    :: "[idt, 'a set, o] => 'a set"      ("(1{_: _ ./ _})")
     1.5  
     1.6  translations
     1.7 -  "PROD x:A. B" => "Pi(A, %x. B)"
     1.8 -  "A -> B"      => "Pi(A, %_. B)"
     1.9 -  "SUM x:A. B"  => "Sigma(A, %x. B)"
    1.10 -  "A * B"       => "Sigma(A, %_. B)"
    1.11 -  "{x: A. B}"   == "Subtype(A, %x. B)"
    1.12 +  "PROD x:A. B" => "CONST Pi(A, %x. B)"
    1.13 +  "A -> B"      => "CONST Pi(A, %_. B)"
    1.14 +  "SUM x:A. B"  => "CONST Sigma(A, %x. B)"
    1.15 +  "A * B"       => "CONST Sigma(A, %_. B)"
    1.16 +  "{x: A. B}"   == "CONST Subtype(A, %x. B)"
    1.17  
    1.18  print_translation {*
    1.19 -  [("Pi", dependent_tr' ("@Pi", "@->")),
    1.20 -   ("Sigma", dependent_tr' ("@Sigma", "@*"))] *}
    1.21 +  [(@{const_syntax Pi}, dependent_tr' ("@Pi", "@->")),
    1.22 +   (@{const_syntax Sigma}, dependent_tr' ("@Sigma", "@*"))] *}
    1.23  
    1.24  axioms
    1.25    Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}"