src/Pure/term.ML
changeset 38980 af73cf0dc31f
parent 35986 b7fcca3d9a44
child 39293 651e5a3e8cfd
     1.1 --- a/src/Pure/term.ML	Wed Sep 01 23:43:45 2010 +0200
     1.2 +++ b/src/Pure/term.ML	Thu Sep 02 00:48:07 2010 +0200
     1.3 @@ -114,7 +114,6 @@
     1.4    val exists_type: (typ -> bool) -> term -> bool
     1.5    val exists_subterm: (term -> bool) -> term -> bool
     1.6    val exists_Const: (string * typ -> bool) -> term -> bool
     1.7 -  val show_question_marks: bool Unsynchronized.ref
     1.8  end;
     1.9  
    1.10  signature TERM =
    1.11 @@ -983,11 +982,8 @@
    1.12  
    1.13  (* display variables *)
    1.14  
    1.15 -val show_question_marks = Unsynchronized.ref true;
    1.16 -
    1.17  fun string_of_vname (x, i) =
    1.18    let
    1.19 -    val question_mark = if ! show_question_marks then "?" else "";
    1.20      val idx = string_of_int i;
    1.21      val dot =
    1.22        (case rev (Symbol.explode x) of
    1.23 @@ -996,9 +992,9 @@
    1.24        | c :: _ => Symbol.is_digit c
    1.25        | _ => true);
    1.26    in
    1.27 -    if dot then question_mark ^ x ^ "." ^ idx
    1.28 -    else if i <> 0 then question_mark ^ x ^ idx
    1.29 -    else question_mark ^ x
    1.30 +    if dot then "?" ^ x ^ "." ^ idx
    1.31 +    else if i <> 0 then "?" ^ x ^ idx
    1.32 +    else "?" ^ x
    1.33    end;
    1.34  
    1.35  fun string_of_vname' (x, ~1) = x