src/Pure/Syntax/lexicon.ML
changeset 1143 0dfb8b437f5d
parent 550 353eea6ec232
child 1507 f600215b6ea7
equal deleted inserted replaced
1142:eb0e2ff8f032 1143:0dfb8b437f5d
   107 
   107 
   108 fun string_of_vname (x, i) =
   108 fun string_of_vname (x, i) =
   109   let
   109   let
   110     val si = string_of_int i;
   110     val si = string_of_int i;
   111   in
   111   in
   112     if is_digit (last_elem (explode x)) then "?" ^ x ^ "." ^ si
   112     (if is_digit (last_elem (explode x)) then "?" ^ x ^ "." ^ si
   113     else if i = 0 then "?" ^ x
   113      else if i = 0 then "?" ^ x
   114     else "?" ^ x ^ si
   114      else "?" ^ x ^ si)
       
   115     handle LIST _ => "?NULL_VARIABLE." ^ si
   115   end;
   116   end;
   116 
   117 
   117 
   118 
   118 
   119 
   119 (** datatype token **)
   120 (** datatype token **)