# 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;