diff -r 670f8e4b5a98 -r cb02d70a2040 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Tue May 17 18:10:44 2005 +0200
+++ b/src/Pure/proof_general.ML	Tue May 17 18:51:16 2005 +0200
@@ -143,7 +143,8 @@
     SOME (x, i) =>
       (case try Syntax.dest_skolem x of
         NONE => tagit var_tag s
-      | SOME x' => tagit skolem_tag (Syntax.string_of_vname (x', i)))
+      | SOME x' => tagit skolem_tag
+          (setmp show_question_marks true Syntax.string_of_vname (x', i)))
   | NONE => tagit var_tag s);
 
 val proof_general_trans =