diff -r 274eaa114c6d -r 32bb237158a5 src/CCL/Term.thy --- 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);