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.
tuned absdummy;
authorwenzelm
Sun, 10 Dec 2006 15:30:40 +0100
changeset 21742 a330e58226d0
parent 21741 5f3d62008bb5
child 21743 fe94c6797c09
tuned absdummy;
src/Pure/term.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/term.ML	Sun Dec 10 15:30:39 2006 +0100
+++ b/src/Pure/term.ML	Sun Dec 10 15:30:40 2006 +0100
@@ -896,7 +896,7 @@
 
 (*Form an abstraction over a free variable.*)
 fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));
-fun absdummy (T, body) = Abs ("uu", T, body);
+fun absdummy (T, body) = Abs (Name.internal "x", T, body);
 
 (*Abstraction over a list of free variables*)
 fun list_abs_free ([ ] ,     t) = t
isabelle