
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);




