src/Pure/term.ML
changeset 32198 9bdd47909ea8
parent 32020 9abf5d66606e
child 32738 15bb09ca0378
     1.1 --- a/src/Pure/term.ML	Sun Jul 26 13:12:52 2009 +0200
     1.2 +++ b/src/Pure/term.ML	Sun Jul 26 13:12:53 2009 +0200
     1.3 @@ -151,6 +151,7 @@
     1.4    val match_bvars: (term * term) * (string * string) list -> (string * string) list
     1.5    val map_abs_vars: (string -> string) -> term -> term
     1.6    val rename_abs: term -> term -> term -> term option
     1.7 +  val lambda_name: string * term -> term -> term
     1.8    val close_schematic_term: term -> term
     1.9    val maxidx_typ: typ -> int -> int
    1.10    val maxidx_typs: typ list -> int -> int
    1.11 @@ -719,14 +720,15 @@
    1.12          | _ => raise Same.SAME);
    1.13    in abs 0 body handle Same.SAME => body end;
    1.14  
    1.15 -fun lambda v t =
    1.16 -  let val x =
    1.17 -    (case v of
    1.18 -      Const (x, _) => Long_Name.base_name x
    1.19 -    | Free (x, _) => x
    1.20 -    | Var ((x, _), _) => x
    1.21 -    | _ => Name.uu)
    1.22 -  in Abs (x, fastype_of v, abstract_over (v, t)) end;
    1.23 +fun term_name (Const (x, _)) = Long_Name.base_name x
    1.24 +  | term_name (Free (x, _)) = x
    1.25 +  | term_name (Var ((x, _), _)) = x
    1.26 +  | term_name _ = Name.uu;
    1.27 +
    1.28 +fun lambda_name (x, v) t =
    1.29 +  Abs (if x = "" then term_name v else x, fastype_of v, abstract_over (v, t));
    1.30 +
    1.31 +fun lambda v t = lambda_name ("", v) t;
    1.32  
    1.33  (*Form an abstraction over a free variable.*)
    1.34  fun absfree (a,T,body) = Abs (a, T, abstract_over (Free (a, T), body));