lambda: abstract over any const;
authorwenzelm
Mon Feb 06 20:59:09 2006 +0100 (2006-02-06)
changeset 189429228bbe9cd4e
parent 18941 18cb1e2ab77d
child 18943 947d3a694654
lambda: abstract over any const;
tuned;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Mon Feb 06 20:59:08 2006 +0100
     1.2 +++ b/src/Pure/term.ML	Mon Feb 06 20:59:09 2006 +0100
     1.3 @@ -758,7 +758,7 @@
     1.4    let
     1.5      val ren = match_bvs (pat, obj, []);
     1.6      fun ren_abs (Abs (x, T, b)) =
     1.7 -          Abs (if_none (AList.lookup (op =) ren x) x, T, ren_abs b)
     1.8 +          Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b)
     1.9        | ren_abs (f $ t) = ren_abs f $ ren_abs t
    1.10        | ren_abs t = t
    1.11    in if null ren then NONE else SOME (ren_abs t) end;
    1.12 @@ -897,9 +897,9 @@
    1.13          | _ => raise SAME);
    1.14    in abs 0 body handle SAME => body end;
    1.15  
    1.16 -fun lambda (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t))
    1.17 +fun lambda (v as Const (x, T)) t = Abs (x, T, abstract_over (v, t))
    1.18 +  | lambda (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t))
    1.19    | lambda (v as Var ((x, _), T)) t = Abs (x, T, abstract_over (v, t))
    1.20 -  | lambda (v as Const ("TYPE", T)) t = Abs ("uu", T, abstract_over (v, t))
    1.21    | lambda v t = raise TERM ("lambda", [v, t]);
    1.22  
    1.23  (*Form an abstraction over a free variable.*)
    1.24 @@ -928,7 +928,7 @@
    1.25        let
    1.26          fun subst (Abs (a, T, body)) = Abs (a, T, subst body)
    1.27            | subst (t $ u) = subst t $ subst u
    1.28 -          | subst t = if_none (AList.lookup (op aconv) inst t) t;
    1.29 +          | subst t = the_default t (AList.lookup (op aconv) inst t);
    1.30        in subst tm end;
    1.31  
    1.32  (*Replace the ATOMIC type Ti by Ui;    inst = [(T1,U1), ..., (Tn,Un)].*)
    1.33 @@ -936,7 +936,7 @@
    1.34    | typ_subst_atomic inst ty =
    1.35        let
    1.36          fun subst (Type (a, Ts)) = Type (a, map subst Ts)
    1.37 -          | subst T = if_none (AList.lookup (op = : typ * typ -> bool) inst T) T;
    1.38 +          | subst T = the_default T (AList.lookup (op = : typ * typ -> bool) inst T);
    1.39        in subst ty end;
    1.40  
    1.41  fun subst_atomic_types [] tm = tm
    1.42 @@ -946,7 +946,7 @@
    1.43    | typ_subst_TVars inst ty =
    1.44        let
    1.45          fun subst (Type (a, Ts)) = Type (a, map subst Ts)
    1.46 -          | subst (T as TVar (xi, _)) = if_none (AList.lookup (op =) inst xi) T
    1.47 +          | subst (T as TVar (xi, _)) = the_default T (AList.lookup (op =) inst xi)
    1.48            | subst T = T;
    1.49        in subst ty end;
    1.50  
    1.51 @@ -957,7 +957,7 @@
    1.52  fun subst_Vars [] tm = tm
    1.53    | subst_Vars inst tm =
    1.54        let
    1.55 -        fun subst (t as Var (xi, _)) = if_none (AList.lookup (op =) inst xi) t
    1.56 +        fun subst (t as Var (xi, _)) = the_default t (AList.lookup (op =) inst xi)
    1.57            | subst (Abs (a, T, t)) = Abs (a, T, subst t)
    1.58            | subst (t $ u) = subst t $ subst u
    1.59            | subst t = t;