# HG changeset patch
# User wenzelm
# Date 1139255947 -3600
# Node ID d8e12bf337a383abe15ef244f4bf2b110943d309
# Parent  18e2a2676d807c2381360d1c376199c4b19350d0
moved (beta_)eta_contract to envir.ML;
tuned;

diff -r 18e2a2676d80 -r d8e12bf337a3 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Mon Feb 06 20:59:06 2006 +0100
+++ b/src/Pure/pattern.ML	Mon Feb 06 20:59:07 2006 +0100
@@ -17,9 +17,7 @@
 sig
   val trace_unify_fail: bool ref
   val aeconv: term * term -> bool
-  val eta_contract: term -> term
   val eta_long: typ list -> term -> term
-  val beta_eta_contract: term -> term
   val eta_contract_atom: term -> term
   val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
   val first_order_match: theory -> term * term
@@ -272,31 +270,6 @@
 fun unify thy = unif thy [];
 
 
-(*Eta-contract a term (fully)*)
-
-fun eta_contract t =
-  let
-    exception SAME;
-    fun eta (Abs (a, T, body)) =
-      ((case eta body of
-          body' as (f $ Bound 0) =>
-            if loose_bvar1 (f, 0) then Abs(a, T, body')
-            else incr_boundvars ~1 f
-        | body' => Abs (a, T, body')) handle SAME =>
-       (case body of
-          (f $ Bound 0) =>
-            if loose_bvar1 (f, 0) then raise SAME
-            else incr_boundvars ~1 f
-        | _ => raise SAME))
-      | eta (f $ t) =
-          (let val f' = eta f
-           in f' $ etah t end handle SAME => f $ eta t)
-      | eta _ = raise SAME
-    and etah t = (eta t handle SAME => t)
-  in etah t end;
-
-val beta_eta_contract = eta_contract o Envir.beta_norm;
-
 (*Eta-contract a term from outside: just enough to reduce it to an atom
 DOESN'T QUITE WORK!
 *)
@@ -476,7 +449,7 @@
       in (abs, t') end;
 
     fun match_rew tm (tm1, tm2) =
-      let val rtm = if_none (Term.rename_abs tm1 tm tm2) tm2 in
+      let val rtm = the_default tm2 (Term.rename_abs tm1 tm tm2) in
         SOME (Envir.subst_vars (match thy (tm1, tm) (Vartab.empty, Vartab.empty)) rtm, rtm)
           handle MATCH => NONE
       end;
@@ -489,16 +462,16 @@
     fun rew1 bounds (Var _) _ = NONE
       | rew1 bounds skel tm = (case rew2 bounds skel tm of
           SOME tm1 => (case rew tm1 of
-              SOME (tm2, skel') => SOME (if_none (rew1 bounds skel' tm2) tm2)
+              SOME (tm2, skel') => SOME (the_default tm2 (rew1 bounds skel' tm2))
             | NONE => SOME tm1)
         | NONE => (case rew tm of
-              SOME (tm1, skel') => SOME (if_none (rew1 bounds skel' tm1) tm1)
+              SOME (tm1, skel') => SOME (the_default tm1 (rew1 bounds skel' tm1))
             | NONE => NONE))
 
     and rew2 bounds skel (tm1 $ tm2) = (case tm1 of
             Abs (_, _, body) =>
               let val tm' = subst_bound (tm2, body)
-              in SOME (if_none (rew2 bounds skel0 tm') tm') end
+              in SOME (the_default tm' (rew2 bounds skel0 tm')) end
           | _ =>
             let val (skel1, skel2) = (case skel of
                 skel1 $ skel2 => (skel1, skel2)
@@ -521,7 +494,7 @@
           end
       | rew2 _ _ _ = NONE;
 
-  in if_none (rew1 0 skel0 tm) tm end;
+  in the_default tm (rew1 0 skel0 tm) end;
 
 end;