# HG changeset patch
# User wenzelm
# Date 1165761053 -3600
# Node ID 41986849fee0caa578e6de05fe9685980bf80e0a
# Parent  3f0e86c92ff3b144c834b073bba75002f9344222
abs/binder_tr': support printing of idtdummy;

diff -r 3f0e86c92ff3 -r 41986849fee0 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Sun Dec 10 15:30:49 2006 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Sun Dec 10 15:30:53 2006 +0100
@@ -246,10 +246,12 @@
     val vars = vars_of tm;
     val body = body_of tm;
     val rev_new_vars = rename_wrt_term body vars;
-  in
-    (map mark_boundT (rev rev_new_vars),
-      subst_bounds (map (mark_bound o #1) rev_new_vars, body))
-  end;
+    fun subst (x, T) b =
+      if can Name.dest_internal x andalso not (Term.loose_bvar1 (b, 0))
+      then (Const ("_idtdummy", T), incr_boundvars ~1 b)
+      else (mark_boundT (x, T), Term.subst_bound (mark_bound x, b));
+    val (rev_vars', body') = fold_map subst rev_new_vars body;
+  in (rev rev_vars', body') end;
 
 
 (*do (partial) eta-contraction before printing*)