src/HOL/Tools/SMT/smt_translate.ML
changeset 42321 ce83c1654b86
parent 42319 9a8ba59aed06
child 43154 72e4753a6677
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Fri Apr 08 19:04:08 2011 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Fri Apr 08 19:04:08 2011 +0200
     1.3 @@ -184,7 +184,7 @@
     1.4      let val Ts = drop i (fst (SMT_Utils.dest_funT k T))
     1.5      in
     1.6        Term.incr_boundvars (length Ts) t
     1.7 -      |> fold_index (fn (i, _) => fn u => u $ Bound i) Ts
     1.8 +      |> fold_rev (fn i => fn u => u $ Bound i) (0 upto length Ts - 1)
     1.9        |> fold_rev (fn T => fn u => Abs (Name.uu, T, u)) Ts
    1.10      end
    1.11  in