# HG changeset patch
# User wenzelm
# Date 1116348676 -7200
# Node ID cb02d70a2040959936c063ac2ea293bc03bb6bc6
# Parent  670f8e4b5a98a253cefd4d412cba93bb0959e8ec
var_or_skolem: always print question mark for vars stemming from skolems;

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 =