# HG changeset patch
# User wenzelm
# Date 1116346238 -7200
# Node ID f00dd5e06ffe2a2b57f3901eb606c220e233e7ca
# Parent  bc6ead9d662875b37fb2a811a22cec4b48f47503
renamed show_var_qmarks to show_question_marks;
var_or_skolem: proper treatment of show_question_marks via Syntax.read_variable;

diff -r bc6ead9d6628 -r f00dd5e06ffe src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Tue May 17 18:10:37 2005 +0200
+++ b/src/Pure/proof_general.ML	Tue May 17 18:10:38 2005 +0200
@@ -139,12 +139,12 @@
   | SOME x' => tagit skolem_tag x');
 
 fun var_or_skolem s =
-  (case Syntax.read_var s of
-    Var ((x, i), _) =>
+  (case Syntax.read_variable s of
+    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)))
-  | _ => tagit var_tag s);
+  | NONE => tagit var_tag s);
 
 val proof_general_trans =
  Syntax.tokentrans_mode proof_generalN
@@ -593,9 +593,9 @@
      ("print-depth", 
       ("Setting for the ML print depth",
        print_depth_option)),
-     ("show-var-qmarks",
+     ("show-question-marks",
       ("Show leading question mark of variable name",
-       bool_option show_var_qmarks))]),
+       bool_option show_question_marks))]),
    ("Tracing",
     [("trace-simplifier", 
       ("Trace simplification rules.",