src/CTT/CTT.thy

   "@-->"    :: "[t,t]=>t"           ("(_ -->/ _)" [31,30] 30)
   "@*"      :: "[t,t]=>t"           ("(_ */ _)" [51,50] 50)
 
 translations
   "PROD x:A. B" => "Prod(A, %x. B)"
-  "A --> B"     => "Prod(A, _K(B))"
+  "A --> B"     => "Prod(A, %_. B)"
   "SUM x:A. B"  => "Sum(A, %x. B)"
-  "A * B"       => "Sum(A, _K(B))"
+  "A * B"       => "Sum(A, %_. B)"
 
 print_translation {*
   [("Prod", dependent_tr' ("@PROD", "@-->")),
    ("Sum", dependent_tr' ("@SUM", "@*"))]
 *}