Term.lambda: abstract over arbitrary closed terms;

--- a/src/Pure/term.ML	Sun Dec 31 15:57:58 2006 +0100
+++ b/src/Pure/term.ML	Tue Jan 02 22:43:04 2007 +0100
@@ -913,13 +913,17 @@
         | _ => raise SAME);
   in abs 0 body handle SAME => body end;
 
-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]);
+fun lambda v t =
+  let val x =
+    (case v of
+      Const (x, _) => NameSpace.base x
+    | Free (x, _) => x
+    | Var ((x, _), _) => x
+    | _ => "uu")
+  in Abs (x, fastype_of v, abstract_over (v, t)) end;
 
 (*Form an abstraction over a free variable.*)
-fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));
+fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body));
 fun absdummy (T, body) = Abs (Name.internal "x", T, body);
 
 (*Abstraction over a list of free variables*)

--- a/src/Pure/thm.ML	Sun Dec 31 15:57:58 2006 +0100
+++ b/src/Pure/thm.ML	Tue Jan 02 22:43:04 2007 +0100
@@ -313,7 +313,7 @@
 fun cabs
   (ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...})
   (ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) =
-    let val t = lambda t1 t2 handle TERM _ => raise CTERM "cabs: malformed first argument" in
+    let val t = Term.lambda t1 t2 in
       Cterm {thy_ref = merge_thys0 ct1 ct2,
         t = t, T = T1 --> T2,
         maxidx = Int.max (maxidx1, maxidx2),