changeset 15992 | cb02d70a2040 |
parent 15985 | f00dd5e06ffe |
child 16022 | 96a9bf7ac18d |
--- 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 =