# HG changeset patch
# User lcp
# Date 762712994 -3600
# Node ID 4cf7139e5b7afbec5bb5f958df96f63e9e532dc0
# Parent  933ec96c522e205c1a01ba7db695bb71e0bf6d37
changed "x" to "uu" for implicit name of the
dependent type variable

diff -r 933ec96c522e -r 4cf7139e5b7a src/Pure/Syntax/sextension.ML
--- a/src/Pure/Syntax/sextension.ML	Tue Mar 01 17:21:47 1994 +0100
+++ b/src/Pure/Syntax/sextension.ML	Thu Mar 03 17:43:14 1994 +0100
@@ -173,7 +173,7 @@
 
 (* nondependent abstraction *)
 
-fun k_tr (*"_K"*) [t] = Abs ("x", dummyT, incr_boundvars 1 t)
+fun k_tr (*"_K"*) [t] = Abs ("uu", dummyT, incr_boundvars 1 t)
   | k_tr (*"_K"*) ts = raise_term "k_tr" ts;