src/Pure/term.ML
changeset 18975 78d650a7e99a
parent 18942 9228bbe9cd4e
child 18976 4efb82669880
     1.1 --- a/src/Pure/term.ML	Tue Feb 07 19:56:58 2006 +0100
     1.2 +++ b/src/Pure/term.ML	Tue Feb 07 19:57:00 2006 +0100
     1.3 @@ -897,7 +897,7 @@
     1.4          | _ => raise SAME);
     1.5    in abs 0 body handle SAME => body end;
     1.6  
     1.7 -fun lambda (v as Const (x, T)) t = Abs (x, T, abstract_over (v, t))
     1.8 +fun lambda (v as Const (x, T)) t = Abs (NameSpace.base x, T, abstract_over (v, t))
     1.9    | lambda (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t))
    1.10    | lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
    1.11    | lambda v t = raise TERM ("lambda", [v, t]);