1.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Mon Apr 23 12:23:23 2012 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Mon Apr 23 12:23:23 2012 +0100
     1.3 @@ -151,6 +151,7 @@
     1.4    val get_file_list : Path.T -> Path.T list
     1.5  
     1.6    val string_of_tptp_term : tptp_term -> string
     1.7 +  val string_of_interpreted_symbol : interpreted_symbol -> string
     1.8    val string_of_tptp_formula : tptp_formula -> string
     1.9  
    1.10  end
    1.11 @@ -420,6 +421,7 @@
    1.12      | EvalEq => "$evaleq"
    1.13      | Is_Int => "$is_int"
    1.14      | Is_Rat => "$is_rat"
    1.15 +    | Distinct => "$distinct"
    1.16      | Apply => "@"
    1.17  
    1.18  and string_of_logic_symbol Equals = "="