src/HOL/Tools/res_clause.ML
changeset 18275 86cefba6d325
parent 18218 9a7ffce389c3
child 18390 aaecdaef4c04
     1.1 --- a/src/HOL/Tools/res_clause.ML	Mon Nov 28 07:15:38 2005 +0100
     1.2 +++ b/src/HOL/Tools/res_clause.ML	Mon Nov 28 07:16:16 2005 +0100
     1.3 @@ -69,6 +69,7 @@
     1.4    val gen_tptp_cls : int * string * string * string -> string
     1.5    val gen_tptp_type_cls : int * string * string * string * int -> string
     1.6    val tptp_of_typeLit : type_literal -> string
     1.7 +
     1.8    end;
     1.9  
    1.10  structure ResClause: RES_CLAUSE =
    1.11 @@ -688,14 +689,16 @@
    1.12    | string_of_term (Fun (name,typs,[])) = name (*Overloaded consts like 0 don't get types!*)
    1.13    | string_of_term (Fun (name,typs,terms)) = 
    1.14        let val terms_as_strings = map string_of_term terms
    1.15 -      in  name ^ (paren_pack (terms_as_strings @ typs))  end
    1.16 +	  val typs' = if !keep_types then typs else []
    1.17 +      in  name ^ (paren_pack (terms_as_strings @ typs'))  end
    1.18    | string_of_term _ = error "string_of_term";      
    1.19  
    1.20  (* before output the string of the predicate, check if the predicate corresponds to an equality or not. *)
    1.21  fun string_of_predicate (Predicate("equal",[typ],terms)) = string_of_equality(typ,terms)
    1.22    | string_of_predicate (Predicate(name,typs,terms)) = 
    1.23        let val terms_as_strings = map string_of_term terms
    1.24 -      in  name ^ (paren_pack (terms_as_strings @ typs))  end
    1.25 +	  val typs' = if !keep_types then typs else []
    1.26 +      in  name ^ (paren_pack (terms_as_strings @ typs'))  end
    1.27    | string_of_predicate _ = error "string_of_predicate";      
    1.28  
    1.29