# HG changeset patch
# User wenzelm
# Date 1139255951 -3600
# Node ID 7d2ed90634775e8d38fb415db6a0686abfdf949f
# Parent  947d3a694654e6b610c92496e40780d9612b8c16
union_tpairs: Library.merge;
Envir.(beta_)eta_contract;
tuned;

diff -r 947d3a694654 -r 7d2ed9063477 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Feb 06 20:59:10 2006 +0100
+++ b/src/Pure/thm.ML	Mon Feb 06 20:59:11 2006 +0100
@@ -255,7 +255,7 @@
 
 (*Destruct abstraction in cterms*)
 fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) =
-      let val (y', t') = Term.dest_abs (if_none a x, T, t) in
+      let val (y', t') = Term.dest_abs (the_default x a, T, t) in
         (Cterm {t = Free (y', T), T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts},
           Cterm {t = t', T = U, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts})
       end
@@ -282,7 +282,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: first arg is not a variable" in
+    let val t = lambda t1 t2 handle TERM _ => raise CTERM "cabs: malformed first argument" in
       Cterm {thy_ref = merge_thys0 ct1 ct2,
         t = t, T = T1 --> T2,
         maxidx = Int.max (maxidx1, maxidx2),
@@ -380,7 +380,7 @@
 fun terms_of_tpairs tpairs = fold_rev (fn (t, u) => cons t o cons u) tpairs [];
 
 fun eq_tpairs ((t, u), (t', u')) = t aconv t' andalso u aconv u';
-val union_tpairs = gen_merge_lists eq_tpairs;
+fun union_tpairs ts us = Library.merge eq_tpairs (ts, us);
 val maxidx_tpairs = fold (fn (t, u) => Term.maxidx_term t #> Term.maxidx_term u);
 
 fun attach_tpairs tpairs prop =
@@ -820,7 +820,7 @@
     shyps = sorts,
     hyps = [],
     tpairs = [],
-    prop = Logic.mk_equals (t, Pattern.eta_contract t)};
+    prop = Logic.mk_equals (t, Envir.eta_contract t)};
 
 (*The abstraction rule.  The Free or Var x must not be free in the hypotheses.
   The bound variable will be named "a" (since x will be something like x320)
@@ -1340,7 +1340,7 @@
                               else Var((y,i),T)
                  | NONE=> t)
           | rename(Abs(x,T,t)) =
-              Abs (if_none (AList.lookup (op =) al x) x, T, rename t)
+              Abs (the_default x (AList.lookup (op =) al x), T, rename t)
           | rename(f$t) = rename f $ rename t
           | rename(t) = t;
         fun strip_ren Ai = strip_apply rename (Ai,B)