| changeset 17781 | 32bb237158a5 |
| parent 17456 | bcf7544875b2 |
| child 19796 | d86e7b1fc472 |
--- a/src/CCL/Term.thy Fri Oct 07 22:59:17 2005 +0200 +++ b/src/CCL/Term.thy Fri Oct 07 22:59:18 2005 +0200 @@ -56,6 +56,7 @@ ML {* (** Quantifier translations: variable binding **) +(* FIXME does not handle "_idtdummy" *) (* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *) fun let_tr [Free(id,T),a,b] = Const("let",dummyT) $ a $ absfree(id,T,b);