# HG changeset patch
# User wenzelm
# Date 857393609 -3600
# Node ID 241fffc25284378b310f77615eac6f035c18d66f
# Parent  c3b86dcd340ad5df62718ed6afd25b6acab992ad
added comment;

diff -r c3b86dcd340a -r 241fffc25284 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Mon Mar 03 13:50:40 1997 +0100
+++ b/src/CCL/Term.thy	Mon Mar 03 13:53:29 1997 +0100
@@ -91,6 +91,8 @@
 
 (** Quantifier translations: variable binding **)
 
+(* 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);
 fun let_tr' [a,Abs(id,T,b)] =
      let val (id',b') = variant_abs(id,T,b)