src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML

   subdirectories. This is only used for testing the parser/interpreter against
   all THF problems.*)
   val get_file_list : Path.T -> Path.T list
 
   val string_of_tptp_term : tptp_term -> string
+  val string_of_interpreted_symbol : interpreted_symbol -> string
   val string_of_tptp_formula : tptp_formula -> string
 
 end
 
 

     | Greater => "$greater"
     | GreaterEq => "$greatereq"
     | EvalEq => "$evaleq"
     | Is_Int => "$is_int"
     | Is_Rat => "$is_rat"
+    | Distinct => "$distinct"
     | Apply => "@"
 
 and string_of_logic_symbol Equals = "="
   | string_of_logic_symbol NEquals = "!="
   | string_of_logic_symbol Or = "|"