src/Pure/pattern.ML
changeset 12817 fcbb6ad5c790
parent 12797 4de06a8f67ef
child 12826 dfb214fa310b
     1.1 --- a/src/Pure/pattern.ML	Fri Jan 18 18:35:39 2002 +0100
     1.2 +++ b/src/Pure/pattern.ML	Fri Jan 18 18:36:19 2002 +0100
     1.3 @@ -424,18 +424,11 @@
     1.4      fun rew (Abs (_, _, body) $ t) = Some (subst_bound (t, body))
     1.5        | rew tm = get_first (match_rew tm) rules;
     1.6  
     1.7 -    fun rew0 (tm as Abs (_, _, tm' $ Bound 0)) =
     1.8 -          if loose_bvar1 (tm', 0) then rew tm
     1.9 -          else
    1.10 -            let val tm'' = incr_boundvars ~1 tm'
    1.11 -            in Some (if_none (rew tm'') tm'') end
    1.12 -      | rew0 tm = rew tm;
    1.13 -
    1.14      fun rew1 tm = (case rew2 tm of
    1.15 -          Some tm1 => (case rew0 tm1 of
    1.16 +          Some tm1 => (case rew tm1 of
    1.17                Some tm2 => Some (if_none (rew1 tm2) tm2)
    1.18              | None => Some tm1)
    1.19 -        | None => (case rew0 tm of
    1.20 +        | None => (case rew tm of
    1.21                Some tm1 => Some (if_none (rew1 tm1) tm1)
    1.22              | None => None))
    1.23