Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
support printing of idtdummy;
authorwenzelm
Sun, 10 Dec 2006 15:30:48 +0100
changeset 21748 7df0f4e08dde
parent 21747 d650305c609a
child 21749 3f0e86c92ff3
support printing of idtdummy;
src/Pure/Syntax/printer.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle