--- 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),