# HG changeset patch
# User wenzelm
# Date 1128718759 -7200
# Node ID b3846df9d643ab06fc7f8701a159c3ad86e38c1a
# Parent  32bb237158a5fee717467dfffcfc9bafffe3cf08
replaced _K by dummy abstraction;

diff -r 32bb237158a5 -r b3846df9d643 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 {*
diff -r 32bb237158a5 -r b3846df9d643 src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Fri Oct 07 22:59:18 2005 +0200
+++ b/src/CTT/CTT.thy	Fri Oct 07 22:59:19 2005 +0200
@@ -64,9 +64,9 @@
 
 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", "@-->")),
diff -r 32bb237158a5 -r b3846df9d643 src/Cube/Cube.thy
--- a/src/Cube/Cube.thy	Fri Oct 07 22:59:18 2005 +0200
+++ b/src/Cube/Cube.thy	Fri Oct 07 22:59:19 2005 +0200
@@ -39,7 +39,7 @@
   ("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, _K(B))"
+  "A -> B"       => "Prod(A, %_. B)"
 
 syntax (xsymbols)
   Trueprop      :: "[context_, typing_] => prop"        ("(_/ \<turnstile> _)")
diff -r 32bb237158a5 -r b3846df9d643 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Oct 07 22:59:18 2005 +0200
+++ b/src/HOL/Finite_Set.thy	Fri Oct 07 22:59:19 2005 +0200
@@ -840,7 +840,7 @@
 
 parse_translation {*
   let
-    fun Setsum_tr [A] = Syntax.const "setsum" $ Abs ("", dummyT, Bound 0) $ A
+    fun Setsum_tr [A] = Syntax.const "setsum" $ Term.absdummy (dummyT, Bound 0) $ A
   in [("_Setsum", Setsum_tr)] end;
 *}
 
diff -r 32bb237158a5 -r b3846df9d643 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Fri Oct 07 22:59:18 2005 +0200
+++ b/src/HOL/Map.thy	Fri Oct 07 22:59:19 2005 +0200
@@ -66,7 +66,7 @@
   --"requires amssymb!"
 
 translations
-  "empty"    => "_K None"
+  "empty"    => "%_. None"
   "empty"    <= "%x. None"
 
   "m(x\<mapsto>\<lambda>y. f)" == "chg_map (\<lambda>y. f) x m"
diff -r 32bb237158a5 -r b3846df9d643 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Fri Oct 07 22:59:18 2005 +0200
+++ b/src/HOL/Product_Type.thy	Fri Oct 07 22:59:19 2005 +0200
@@ -128,7 +128,7 @@
      The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *)
 
   "SIGMA x:A. B" => "Sigma A (%x. B)"
-  "A <*> B"      => "Sigma A (_K B)"
+  "A <*> B"      => "Sigma A (%_. B)"
 
 (* reconstructs pattern from (nested) splits, avoiding eta-contraction of body*)
 (* works best with enclosing "let", if "let" does not avoid eta-contraction   *)
diff -r 32bb237158a5 -r b3846df9d643 src/ZF/QPair.thy
--- a/src/ZF/QPair.thy	Fri Oct 07 22:59:18 2005 +0200
+++ b/src/ZF/QPair.thy	Fri Oct 07 22:59:19 2005 +0200
@@ -46,7 +46,7 @@
 
 translations
   "QSUM x:A. B"  => "QSigma(A, %x. B)"
-  "A <*> B"      => "QSigma(A, _K(B))"
+  "A <*> B"      => "QSigma(A, %_. B)"
 
 constdefs
   qsum    :: "[i,i]=>i"                         (infixr "<+>" 65)
diff -r 32bb237158a5 -r b3846df9d643 src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Fri Oct 07 22:59:18 2005 +0200
+++ b/src/ZF/ZF.thy	Fri Oct 07 22:59:19 2005 +0200
@@ -131,8 +131,8 @@
   "UN x:A. B"   == "Union({B. x:A})"
   "PROD x:A. B" => "Pi(A, %x. B)"
   "SUM x:A. B"  => "Sigma(A, %x. B)"
-  "A -> B"      => "Pi(A, _K(B))"
-  "A * B"       => "Sigma(A, _K(B))"
+  "A -> B"      => "Pi(A, %_. B)"
+  "A * B"       => "Sigma(A, %_. B)"
   "lam x:A. f"  == "Lambda(A, %x. f)"
   "ALL x:A. P"  == "Ball(A, %x. P)"
   "EX x:A. P"   == "Bex(A, %x. P)"