author | wenzelm |
Mon, 03 Mar 1997 13:53:29 +0100 | |
changeset 2709 | 241fffc25284 |
parent 2708 | c3b86dcd340a |
child 2710 | 3b26198fdaa5 |
src/CCL/Term.thy | file | annotate | diff | comparison | revisions |
--- 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)