changeset 49660 | de49d9b4d7bc |
parent 44241 | 7943b69f0188 |
child 51670 | d721d21e6374 |
--- a/src/CCL/Term.thy Sat Sep 29 16:51:04 2012 +0200 +++ b/src/CCL/Term.thy Sat Sep 29 18:23:46 2012 +0200 @@ -56,7 +56,7 @@ (** Quantifier translations: variable binding **) (* FIXME does not handle "_idtdummy" *) -(* FIXME should use Syntax_Trans.mark_bound(T), Syntax_Trans.variant_abs' *) +(* FIXME should use Syntax_Trans.mark_bound, Syntax_Trans.variant_abs' *) fun let_tr [Free x, a, b] = Const(@{const_syntax let},dummyT) $ a $ absfree x b; fun let_tr' [a,Abs(id,T,b)] =