# HG changeset patch
# User wenzelm
# Date 928518664 -7200
# Node ID 99797f2652d1290a741f4a0bbf6d0d72738c8183
# Parent  34270fe45516eefd87e40109ce640b9c2f006e78
print "..." variable;

diff -r 34270fe45516 -r 99797f2652d1 src/Pure/Syntax/printer.ML
--- 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