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.
print "..." variable;
authorwenzelm
Fri, 04 Jun 1999 19:51:04 +0200
changeset 6767 99797f2652d1
parent 6766 34270fe45516
child 6768 26d64339c25a
print "..." variable;
src/Pure/Syntax/printer.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Syntax/printer.ML	Fri Jun 04 16:17:51 1999 +0200
+++ b/src/Pure/Syntax/printer.ML	Fri Jun 04 19:51:04 1999 +0200
@@ -102,7 +102,9 @@
 fun mark_freevars (t $ u) = mark_freevars t $ mark_freevars u
   | mark_freevars (Abs (x, T, t)) = Abs (x, T, mark_freevars t)
   | mark_freevars (t as Free _) = Lexicon.const "_free" $ t
-  | mark_freevars (t as Var _) =  Lexicon.const "_var" $ t
+  | mark_freevars (t as Var (xi, T)) =
+      if xi = SynExt.dddot_indexname then Const ("_DDDOT", T)
+      else Lexicon.const "_var" $ t
   | mark_freevars a = a;
 
 fun ast_of_term trf no_freeTs show_types show_sorts tm =
@@ -124,9 +126,7 @@
           let
             val (t1', seen') = prune_typs (t1, seen);
             val (t2', seen'') = prune_typs (t2, seen');
-          in
-            (t1' $ t2', seen'')
-          end;
+          in (t1' $ t2', seen'') end;
 
     fun ast_of tm =
       (case strip_comb tm of
isabelle