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.
lambda: abstract over TYPE argument, too;
authorwenzelm
Tue, 31 Jan 2006 18:19:26 +0100
changeset 18871 ca48320f6619
parent 18870 020e242c02a0
child 18872 020044cf1510
lambda: abstract over TYPE argument, too;
src/Pure/term.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/term.ML	Tue Jan 31 18:19:25 2006 +0100
+++ b/src/Pure/term.ML	Tue Jan 31 18:19:26 2006 +0100
@@ -895,6 +895,7 @@
 
 fun lambda (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t))
   | lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
+  | lambda (v as Const ("TYPE", T)) t = Abs ("uu", T, abstract_over (v, t))
   | lambda v t = raise TERM ("lambda", [v, t]);
 
 (*Form an abstraction over a free variable.*)
isabelle