summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | boehmes |

Thu, 16 Dec 2010 12:33:06 +0100 | |

changeset 41196 | d23af676f9f8 |

parent 41195 | f59491d56327 |

child 41197 | edab1efe0a70 |

fixed introduction of explicit application function: bound variables always need explicit application if they are applied to some term

--- a/src/HOL/Tools/SMT/smt_translate.ML Thu Dec 16 12:07:36 2010 +0100 +++ b/src/HOL/Tools/SMT/smt_translate.ML Thu Dec 16 12:33:06 2010 +0100 @@ -361,7 +361,7 @@ | (u as Bound i, ts) => appl0 (nth arities i) (map (traverse env) ts) (u, nth Ts i) | (Abs (n, T, u), ts) => - let val env' = (get_arities 0 u [] :: arities, T :: Ts) + let val env' = (get_arities 0 u [0] :: arities, T :: Ts) in traverses env (Abs (n, T, traverse env' u)) ts end | (u, ts) => traverses env u ts) and traverses env t ts = Term.list_comb (t, map (traverse env) ts)