src/Tools/eqsubst.ML
changeset 52242 2d634bfa1bbf
parent 52240 066c2ff17f7c
child 52246 54c0d4128b30
     1.1 --- a/src/Tools/eqsubst.ML	Thu May 30 16:48:50 2013 +0200
     1.2 +++ b/src/Tools/eqsubst.ML	Thu May 30 16:53:32 2013 +0200
     1.3 @@ -110,14 +110,14 @@
     1.4  fun mk_fake_bound_name n = ":b_" ^ n;
     1.5  fun fakefree_badbounds Ts t =
     1.6    let val (FakeTs, Ts, newnames) =
     1.7 -    List.foldr (fn ((n, ty), (FakeTs, Ts, usednames)) =>
     1.8 +    fold_rev (fn (n, ty) => fn (FakeTs, Ts, usednames) =>
     1.9        let
    1.10          val newname = singleton (Name.variant_list usednames) n
    1.11        in
    1.12          ((mk_fake_bound_name newname, ty) :: FakeTs,
    1.13            (newname, ty) :: Ts,
    1.14            newname :: usednames)
    1.15 -      end) ([], [], []) Ts
    1.16 +      end) Ts ([], [], [])
    1.17    in (FakeTs, Ts, Term.subst_bounds (map Free FakeTs, t)) end;
    1.18  
    1.19  (* before matching we need to fake the bound vars that are missing an