src/CCL/Term.thy
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)] =