src/Pure/term.ML

         | _ => raise SAME);
   in abs 0 body handle SAME => body end;
 
 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.*)
 fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));
 fun absdummy (T, body) = Abs ("uu", T, body);