diff -r 593af1a1068b -r 78d650a7e99a src/Pure/term.ML
--- a/src/Pure/term.ML	Tue Feb 07 19:56:58 2006 +0100
+++ b/src/Pure/term.ML	Tue Feb 07 19:57:00 2006 +0100
@@ -897,7 +897,7 @@
         | _ => raise SAME);
   in abs 0 body handle SAME => body end;
 
-fun lambda (v as Const (x, T)) t = Abs (x, T, abstract_over (v, t))
+fun lambda (v as Const (x, T)) t = Abs (NameSpace.base x, T, abstract_over (v, t))
   | 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 t = raise TERM ("lambda", [v, t]);