src/Pure/term.ML
changeset 18871 ca48320f6619
parent 18847 5fac129ae936
child 18893 2dbf73278b0e
     1.1 --- a/src/Pure/term.ML	Tue Jan 31 18:19:25 2006 +0100
     1.2 +++ b/src/Pure/term.ML	Tue Jan 31 18:19:26 2006 +0100
     1.3 @@ -895,6 +895,7 @@
     1.4  
     1.5  fun lambda (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t))
     1.6    | lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
     1.7 +  | lambda (v as Const ("TYPE", T)) t = Abs ("uu", T, abstract_over (v, t))
     1.8    | lambda v t = raise TERM ("lambda", [v, t]);
     1.9  
    1.10  (*Form an abstraction over a free variable.*)