src/Pure/proof_general.ML
changeset 15985 f00dd5e06ffe
parent 15964 f2074e12d1d4
child 15992 cb02d70a2040
     1.1 --- a/src/Pure/proof_general.ML	Tue May 17 18:10:37 2005 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Tue May 17 18:10:38 2005 +0200
     1.3 @@ -139,12 +139,12 @@
     1.4    | SOME x' => tagit skolem_tag x');
     1.5  
     1.6  fun var_or_skolem s =
     1.7 -  (case Syntax.read_var s of
     1.8 -    Var ((x, i), _) =>
     1.9 +  (case Syntax.read_variable s of
    1.10 +    SOME (x, i) =>
    1.11        (case try Syntax.dest_skolem x of
    1.12          NONE => tagit var_tag s
    1.13        | SOME x' => tagit skolem_tag (Syntax.string_of_vname (x', i)))
    1.14 -  | _ => tagit var_tag s);
    1.15 +  | NONE => tagit var_tag s);
    1.16  
    1.17  val proof_general_trans =
    1.18   Syntax.tokentrans_mode proof_generalN
    1.19 @@ -593,9 +593,9 @@
    1.20       ("print-depth", 
    1.21        ("Setting for the ML print depth",
    1.22         print_depth_option)),
    1.23 -     ("show-var-qmarks",
    1.24 +     ("show-question-marks",
    1.25        ("Show leading question mark of variable name",
    1.26 -       bool_option show_var_qmarks))]),
    1.27 +       bool_option show_question_marks))]),
    1.28     ("Tracing",
    1.29      [("trace-simplifier", 
    1.30        ("Trace simplification rules.",