# HG changeset patch
# User mengj
# Date 1133158576 -3600
# Node ID 86cefba6d3255425081c05fa5fca09be38a81265
# Parent  bbca1d2da0e9b71356b53b97f957822b511ff999
Only output types if !keep_types is true.

diff -r bbca1d2da0e9 -r 86cefba6d325 src/HOL/Tools/res_clause.ML
--- a/src/HOL/Tools/res_clause.ML	Mon Nov 28 07:15:38 2005 +0100
+++ b/src/HOL/Tools/res_clause.ML	Mon Nov 28 07:16:16 2005 +0100
@@ -69,6 +69,7 @@
   val gen_tptp_cls : int * string * string * string -> string
   val gen_tptp_type_cls : int * string * string * string * int -> string
   val tptp_of_typeLit : type_literal -> string
+
   end;
 
 structure ResClause: RES_CLAUSE =
@@ -688,14 +689,16 @@
   | string_of_term (Fun (name,typs,[])) = name (*Overloaded consts like 0 don't get types!*)
   | string_of_term (Fun (name,typs,terms)) = 
       let val terms_as_strings = map string_of_term terms
-      in  name ^ (paren_pack (terms_as_strings @ typs))  end
+	  val typs' = if !keep_types then typs else []
+      in  name ^ (paren_pack (terms_as_strings @ typs'))  end
   | string_of_term _ = error "string_of_term";      
 
 (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *)
 fun string_of_predicate (Predicate("equal",[typ],terms)) = string_of_equality(typ,terms)
   | string_of_predicate (Predicate(name,typs,terms)) = 
       let val terms_as_strings = map string_of_term terms
-      in  name ^ (paren_pack (terms_as_strings @ typs))  end
+	  val typs' = if !keep_types then typs else []
+      in  name ^ (paren_pack (terms_as_strings @ typs'))  end
   | string_of_predicate _ = error "string_of_predicate";