| changeset 18871 | ca48320f6619 |
| parent 18847 | 5fac129ae936 |
| child 18893 | 2dbf73278b0e |
--- 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.*)