src/CCL/Type.thy

--- a/src/CCL/Type.thy	Fri Oct 07 22:59:18 2005 +0200
+++ b/src/CCL/Type.thy	Fri Oct 07 22:59:19 2005 +0200
@@ -41,9 +41,9 @@
 
 translations
   "PROD x:A. B" => "Pi(A, %x. B)"
-  "A -> B"      => "Pi(A, _K(B))"
+  "A -> B"      => "Pi(A, %_. B)"
   "SUM x:A. B"  => "Sigma(A, %x. B)"
-  "A * B"       => "Sigma(A, _K(B))"
+  "A * B"       => "Sigma(A, %_. B)"
   "{x: A. B}"   == "Subtype(A, %x. B)"
 
 print_translation {*