# HG changeset patch
# User wenzelm
# Date 1011375379 -3600
# Node ID fcbb6ad5c79093c5d7125d31884b9ac235a6eb6c
# Parent  668073849ca99fabe3e31704cfc9193746dcd5e6
rewrite_term: removed rew0, so no on-the-fly eta-contraction;

diff -r 668073849ca9 -r fcbb6ad5c790 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Fri Jan 18 18:35:39 2002 +0100
+++ b/src/Pure/pattern.ML	Fri Jan 18 18:36:19 2002 +0100
@@ -424,18 +424,11 @@
     fun rew (Abs (_, _, body) $ t) = Some (subst_bound (t, body))
       | rew tm = get_first (match_rew tm) rules;
 
-    fun rew0 (tm as Abs (_, _, tm' $ Bound 0)) =
-          if loose_bvar1 (tm', 0) then rew tm
-          else
-            let val tm'' = incr_boundvars ~1 tm'
-            in Some (if_none (rew tm'') tm'') end
-      | rew0 tm = rew tm;
-
     fun rew1 tm = (case rew2 tm of
-          Some tm1 => (case rew0 tm1 of
+          Some tm1 => (case rew tm1 of
               Some tm2 => Some (if_none (rew1 tm2) tm2)
             | None => Some tm1)
-        | None => (case rew0 tm of
+        | None => (case rew tm of
               Some tm1 => Some (if_none (rew1 tm1) tm1)
             | None => None))