# 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)