Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
changed "x" to "uu" for implicit name of the
authorlcp
Thu, 03 Mar 1994 17:43:14 +0100
changeset 276 4cf7139e5b7a
parent 275 933ec96c522e
child 277 4abe17e92130
changed "x" to "uu" for implicit name of the dependent type variable
src/Pure/Syntax/sextension.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle