strip_abs_eta: proper use of Name.context;
authorwenzelm
Thu Jul 13 13:42:00 2006 +0200 (2006-07-13)
changeset 2012227255556b762
parent 20121 848fc1a1d355
child 20123 88fa41273824
strip_abs_eta: proper use of Name.context;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Thu Jul 13 13:41:57 2006 +0200
     1.2 +++ b/src/Pure/term.ML	Thu Jul 13 13:42:00 2006 +0200
     1.3 @@ -816,20 +816,20 @@
     1.4    of bound variables and implicit eta-expansion*)
     1.5  fun strip_abs_eta k t =
     1.6    let
     1.7 -    val used = fold_aterms (fn Free (v, _) => cons v | _ => I) t [];
     1.8 +    val used = fold_aterms (fn Free (v, _) => Name.declare v | _ => I) t Name.context;
     1.9      fun strip_abs t (0, used) = (([], t), (0, used))
    1.10        | strip_abs (Abs (v, T, t)) (k, used) =
    1.11            let
    1.12 -            val v' = Name.variant used v;
    1.13 +            val ([v'], used') = Name.variants [v] used;
    1.14              val t' = subst_bound (Free (v, T), t);
    1.15 -            val ((vs, t''), (k', used')) = strip_abs t' (k - 1, v' :: used);
    1.16 -          in (((v', T) :: vs, t''), (k', used')) end
    1.17 +            val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used');
    1.18 +          in (((v', T) :: vs, t''), (k', used'')) end
    1.19        | strip_abs t (k, used) = (([], t), (k, used));
    1.20      fun expand_eta [] t _ = ([], t)
    1.21        | expand_eta (T::Ts) t used =
    1.22            let
    1.23 -            val v = hd (Name.invent_list used "a" 1)
    1.24 -            val (vs, t') = expand_eta Ts (t $ Free (v, T)) (v :: used);
    1.25 +            val ([v], used') = Name.variants [""] used;
    1.26 +            val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
    1.27            in ((v, T) :: vs, t') end;
    1.28      val ((vs1, t'), (k', used')) = strip_abs t (k, used);
    1.29      val Ts = (fst o chop k' o fst o strip_type o fastype_of) t';