Term.lambda: abstract over arbitrary closed terms;
authorwenzelm
Tue Jan 02 22:43:04 2007 +0100 (2007-01-02)
changeset 219751152dc45d591
parent 21974 c4e4d34fbc60
child 21976 1f608af40542
Term.lambda: abstract over arbitrary closed terms;
src/Pure/term.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/term.ML	Sun Dec 31 15:57:58 2006 +0100
     1.2 +++ b/src/Pure/term.ML	Tue Jan 02 22:43:04 2007 +0100
     1.3 @@ -913,13 +913,17 @@
     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 (NameSpace.base x, T, abstract_over (v, t))
     1.8 -  | lambda (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t))
     1.9 -  | lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
    1.10 -  | lambda v t = raise TERM ("lambda", [v, t]);
    1.11 +fun lambda v t =
    1.12 +  let val x =
    1.13 +    (case v of
    1.14 +      Const (x, _) => NameSpace.base x
    1.15 +    | Free (x, _) => x
    1.16 +    | Var ((x, _), _) => x
    1.17 +    | _ => "uu")
    1.18 +  in Abs (x, fastype_of v, abstract_over (v, t)) end;
    1.19  
    1.20  (*Form an abstraction over a free variable.*)
    1.21 -fun absfree (a,T,body) = Abs(a, T, abstract_over (Free(a,T), body));
    1.22 +fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body));
    1.23  fun absdummy (T, body) = Abs (Name.internal "x", T, body);
    1.24  
    1.25  (*Abstraction over a list of free variables*)
     2.1 --- a/src/Pure/thm.ML	Sun Dec 31 15:57:58 2006 +0100
     2.2 +++ b/src/Pure/thm.ML	Tue Jan 02 22:43:04 2007 +0100
     2.3 @@ -313,7 +313,7 @@
     2.4  fun cabs
     2.5    (ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...})
     2.6    (ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) =
     2.7 -    let val t = lambda t1 t2 handle TERM _ => raise CTERM "cabs: malformed first argument" in
     2.8 +    let val t = Term.lambda t1 t2 in
     2.9        Cterm {thy_ref = merge_thys0 ct1 ct2,
    2.10          t = t, T = T1 --> T2,
    2.11          maxidx = Int.max (maxidx1, maxidx2),