src/Pure/Syntax/syn_trans.ML
changeset 21750 41986849fee0
parent 21535 07f8cd0d7962
child 21773 0038f5fc2065
     1.1 --- a/src/Pure/Syntax/syn_trans.ML	Sun Dec 10 15:30:49 2006 +0100
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Sun Dec 10 15:30:53 2006 +0100
     1.3 @@ -246,10 +246,12 @@
     1.4      val vars = vars_of tm;
     1.5      val body = body_of tm;
     1.6      val rev_new_vars = rename_wrt_term body vars;
     1.7 -  in
     1.8 -    (map mark_boundT (rev rev_new_vars),
     1.9 -      subst_bounds (map (mark_bound o #1) rev_new_vars, body))
    1.10 -  end;
    1.11 +    fun subst (x, T) b =
    1.12 +      if can Name.dest_internal x andalso not (Term.loose_bvar1 (b, 0))
    1.13 +      then (Const ("_idtdummy", T), incr_boundvars ~1 b)
    1.14 +      else (mark_boundT (x, T), Term.subst_bound (mark_bound x, b));
    1.15 +    val (rev_vars', body') = fold_map subst rev_new_vars body;
    1.16 +  in (rev rev_vars', body') end;
    1.17  
    1.18  
    1.19  (*do (partial) eta-contraction before printing*)