src/Pure/term.ML
changeset 43326 47cf4bc789aa
parent 43324 2b47822868e4
child 43329 84472e198515
     1.1 --- a/src/Pure/term.ML	Thu Jun 09 17:46:25 2011 +0200
     1.2 +++ b/src/Pure/term.ML	Thu Jun 09 17:51:49 2011 +0200
     1.3 @@ -514,7 +514,8 @@
     1.4  val declare_term_frees = fold_aterms (fn Free (x, _) => Name.declare x | _ => I);
     1.5  
     1.6  fun variant_frees t frees =
     1.7 -  fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees;
     1.8 +  fst (fold_map Name.variant (map fst frees) (declare_term_names t Name.context)) ~~
     1.9 +    map snd frees;
    1.10  
    1.11  fun rename_wrt_term t frees = rev (variant_frees t frees);  (*reversed result!*)
    1.12  
    1.13 @@ -705,7 +706,7 @@
    1.14      fun strip_abs t (0, used) = (([], t), (0, used))
    1.15        | strip_abs (Abs (v, T, t)) (k, used) =
    1.16            let
    1.17 -            val ([v'], used') = Name.variants [v] used;
    1.18 +            val (v', used') = Name.variant v used;
    1.19              val t' = subst_bound (Free (v', T), t);
    1.20              val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used');
    1.21            in (((v', T) :: vs, t''), (k', used'')) end
    1.22 @@ -713,7 +714,7 @@
    1.23      fun expand_eta [] t _ = ([], t)
    1.24        | expand_eta (T::Ts) t used =
    1.25            let
    1.26 -            val ([v], used') = Name.variants [""] used;
    1.27 +            val (v, used') = Name.variant "" used;
    1.28              val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
    1.29            in ((v, T) :: vs, t') end;
    1.30      val ((vs1, t'), (k', used')) = strip_abs t (k, used);