src/Pure/pattern.ML
 changeset 12797 4de06a8f67ef parent 12784 bab3b002cbbb child 12817 fcbb6ad5c790
```     1.1 --- a/src/Pure/pattern.ML	Thu Jan 17 20:59:46 2002 +0100
1.2 +++ b/src/Pure/pattern.ML	Thu Jan 17 21:00:38 2002 +0100
1.3 @@ -228,15 +228,26 @@
1.4
1.5  (*Eta-contract a term (fully)*)
1.6
1.7 -(* copying: *)
1.8 -fun eta_contract (Abs(a,T,body)) =
1.9 -      (case  eta_contract body  of
1.10 -        body' as (f \$ Bound 0) =>
1.11 -          if loose_bvar1(f,0) then Abs(a,T,body')
1.12 -          else incr_boundvars ~1 f
1.13 -      | body' => Abs(a,T,body'))
1.14 -  | eta_contract(f\$t) = eta_contract f \$ eta_contract t
1.15 -  | eta_contract t = t;
1.16 +fun eta_contract t =
1.17 +  let
1.18 +    exception SAME;
1.19 +    fun eta (Abs (a, T, body)) =
1.20 +      ((case eta body of
1.21 +          body' as (f \$ Bound 0) =>
1.22 +	    if loose_bvar1 (f, 0) then Abs(a, T, body')
1.23 +	    else incr_boundvars ~1 f
1.24 +        | body' => Abs (a, T, body')) handle SAME =>
1.25 +       (case body of
1.26 +          (f \$ Bound 0) =>
1.27 +	    if loose_bvar1 (f, 0) then raise SAME
1.28 +	    else incr_boundvars ~1 f
1.29 +        | _ => raise SAME))
1.30 +      | eta (f \$ t) =
1.31 +          (let val f' = eta f
1.32 +           in f' \$ etah t end handle SAME => f \$ eta t)
1.33 +      | eta _ = raise SAME
1.34 +    and etah t = (eta t handle SAME => t)
1.35 +  in etah t end;
1.36
1.37  val beta_eta_contract = eta_contract o Envir.beta_norm;
1.38
1.39 @@ -400,9 +411,16 @@
1.40
1.41  fun rewrite_term tsig rules tm =
1.42    let
1.43 +    val rhs_names =
1.44 +      foldr (fn ((_, rhs), names) => add_term_free_names (rhs, names)) (rules, []);
1.45 +    fun variant_absfree (x, T, t) =
1.46 +      let
1.47 +        val x' = variant (add_term_free_names (t, rhs_names)) x;
1.48 +        val t' = subst_bound (Free (x', T), t);
1.49 +      in (fn u => Abs (x, T, abstract_over (Free (x', T), u)), t') end;
1.50 +
1.51      fun match_rew tm (tm1, tm2) =
1.52        Some (subst_vars (match tsig (tm1, tm)) tm2) handle MATCH => None;
1.53 -
1.54      fun rew (Abs (_, _, body) \$ t) = Some (subst_bound (t, body))
1.55        | rew tm = get_first (match_rew tm) rules;
1.56
1.57 @@ -432,11 +450,14 @@
1.58              | None => (case rew1 tm2 of
1.59                    Some tm2' => Some (tm1 \$ tm2')
1.60                  | None => None)))
1.61 -      | rew2 (Abs (x, T, tm)) = (case rew1 tm of
1.62 -            Some tm' => Some (Abs (x, T, tm'))
1.63 -          | None => None)
1.64 +      | rew2 (Abs (x, T, tm)) =
1.65 +          let val (abs, tm') = variant_absfree (x, T, tm) in
1.66 +            (case rew1 tm' of
1.67 +              Some tm'' => Some (abs tm'')
1.68 +            | None => None)
1.69 +          end
1.70        | rew2 _ = None
1.71
1.72 -  in if_none (rew1 tm) tm end;
1.73 +  in if_none (timeap_msg "FIXME: rewrite_term" rew1 tm) tm end;
1.74
1.75  end;
```