src/CCL/Term.thy
changeset 2709 241fffc25284
parent 1474 3f7d67927fe2
child 3837 d7f033c74b38
equal deleted inserted replaced
2708:c3b86dcd340a 2709:241fffc25284
    89 
    89 
    90 ML
    90 ML
    91 
    91 
    92 (** Quantifier translations: variable binding **)
    92 (** Quantifier translations: variable binding **)
    93 
    93 
       
    94 (* FIXME should use Syntax.mark_bound(T), Syntax.variant_abs' *)
       
    95 
    94 fun let_tr [Free(id,T),a,b] = Const("let",dummyT) $ a $ absfree(id,T,b);
    96 fun let_tr [Free(id,T),a,b] = Const("let",dummyT) $ a $ absfree(id,T,b);
    95 fun let_tr' [a,Abs(id,T,b)] =
    97 fun let_tr' [a,Abs(id,T,b)] =
    96      let val (id',b') = variant_abs(id,T,b)
    98      let val (id',b') = variant_abs(id,T,b)
    97      in Const("@let",dummyT) $ Free(id',T) $ a $ b' end;
    99      in Const("@let",dummyT) $ Free(id',T) $ a $ b' end;
    98 
   100