# HG changeset patch
# User wenzelm
# Date 1139255949 -3600
# Node ID 9228bbe9cd4e3a1b783afbc873cbe30cbfb4447d
# Parent  18cb1e2ab77d9122f923b866a924dfcccc615aa7
lambda: abstract over any const;
tuned;

diff -r 18cb1e2ab77d -r 9228bbe9cd4e src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Feb 06 20:59:08 2006 +0100
+++ b/src/Pure/term.ML	Mon Feb 06 20:59:09 2006 +0100
@@ -758,7 +758,7 @@
   let
     val ren = match_bvs (pat, obj, []);
     fun ren_abs (Abs (x, T, b)) =
-          Abs (if_none (AList.lookup (op =) ren x) x, T, ren_abs b)
+          Abs (the_default x (AList.lookup (op =) ren x), T, ren_abs b)
       | ren_abs (f $ t) = ren_abs f $ ren_abs t
       | ren_abs t = t
   in if null ren then NONE else SOME (ren_abs t) end;
@@ -897,9 +897,9 @@
         | _ => raise SAME);
   in abs 0 body handle SAME => body end;
 
-fun lambda (v as Free (x, T)) t = Abs (x, T, abstract_over (v, t))
+fun lambda (v as Const (x, T)) t = Abs (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 as Const ("TYPE", T)) t = Abs ("uu", T, abstract_over (v, t))
   | lambda v t = raise TERM ("lambda", [v, t]);
 
 (*Form an abstraction over a free variable.*)
@@ -928,7 +928,7 @@
       let
         fun subst (Abs (a, T, body)) = Abs (a, T, subst body)
           | subst (t $ u) = subst t $ subst u
-          | subst t = if_none (AList.lookup (op aconv) inst t) t;
+          | subst t = the_default t (AList.lookup (op aconv) inst t);
       in subst tm end;
 
 (*Replace the ATOMIC type Ti by Ui;    inst = [(T1,U1), ..., (Tn,Un)].*)
@@ -936,7 +936,7 @@
   | typ_subst_atomic inst ty =
       let
         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
-          | subst T = if_none (AList.lookup (op = : typ * typ -> bool) inst T) T;
+          | subst T = the_default T (AList.lookup (op = : typ * typ -> bool) inst T);
       in subst ty end;
 
 fun subst_atomic_types [] tm = tm
@@ -946,7 +946,7 @@
   | typ_subst_TVars inst ty =
       let
         fun subst (Type (a, Ts)) = Type (a, map subst Ts)
-          | subst (T as TVar (xi, _)) = if_none (AList.lookup (op =) inst xi) T
+          | subst (T as TVar (xi, _)) = the_default T (AList.lookup (op =) inst xi)
           | subst T = T;
       in subst ty end;
 
@@ -957,7 +957,7 @@
 fun subst_Vars [] tm = tm
   | subst_Vars inst tm =
       let
-        fun subst (t as Var (xi, _)) = if_none (AList.lookup (op =) inst xi) t
+        fun subst (t as Var (xi, _)) = the_default t (AList.lookup (op =) inst xi)
           | subst (Abs (a, T, t)) = Abs (a, T, subst t)
           | subst (t $ u) = subst t $ subst u
           | subst t = t;