# HG changeset patch
# User wenzelm
# Date 1165761048 -3600
# Node ID 7df0f4e08dde72753e7a4cc42184df26aac72b55
# Parent  d650305c609aa5c6cb2dd09cf56d04713a7cdf7c
support printing of idtdummy;

diff -r d650305c609a -r 7df0f4e08dde src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Sun Dec 10 15:30:46 2006 +0100
+++ b/src/Pure/Syntax/printer.ML	Sun Dec 10 15:30:48 2006 +0100
@@ -147,10 +147,12 @@
         (t as Abs _, ts) => Ast.mk_appl (ast_of (SynTrans.abs_tr' t)) (map ast_of ts)
       | ((c as Const ("_free", _)), Free (x, T) :: ts) =>
           Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
+      | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
+          Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts)
       | ((c as Const ("_bound", _)), Free (x, T) :: ts) =>
           Ast.mk_appl (constrain (c $ Lexicon.free x) T) (map ast_of ts)
-      | ((c as Const ("_var", _)), Var (xi, T) :: ts) =>
-          Ast.mk_appl (constrain (c $ Lexicon.var xi) T) (map ast_of ts)
+      | (Const ("_idtdummy", T), ts) =>
+          Ast.mk_appl (constrain (Lexicon.const "_idtdummy") T) (map ast_of ts)
       | (c' as Const (c, T), ts) =>
           if show_all_types
           then Ast.mk_appl (constrain c' T) (map ast_of ts)