# HG changeset patch
# User mengj
# Date 1132294200 -3600
# Node ID 9d476d1054d74eae3d3106924d3573043720697d
# Parent  d236379ea408850c64440678c9e61b877cd95c84
-- terms are fully typed.
-- only the top-level boolean terms are predicates.

diff -r d236379ea408 -r 9d476d1054d7 src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Fri Nov 18 07:08:54 2005 +0100
+++ b/src/HOL/Tools/res_hol_clause.ML	Fri Nov 18 07:10:00 2005 +0100
@@ -349,6 +349,8 @@
 (**********************************************************************)
 
 val keep_types = ref true;
+val include_combS = ref false;
+
 
 val type_wrapper = "typeinfo";
 
@@ -365,27 +367,25 @@
 
 
 (* convert literals of clauses into strings *)
-fun string_of_combterm (CombConst(c,tp)) = 
-    if tp = bool_tp then c else put_type(c,tp)
-  | string_of_combterm (CombFree(v,tp)) = 
-    if tp = bool_tp then v else put_type(v,tp)
-  | string_of_combterm (CombVar(v,tp)) = 
-    if tp = bool_tp then v else put_type(v,tp)
-  | string_of_combterm (CombApp(t1,t2,tp)) = 
-    let val s1 = string_of_combterm t1
-	val s2 = string_of_combterm t2
+fun string_of_combterm _ (CombConst(c,tp)) = put_type(c,tp)
+  | string_of_combterm _ (CombFree(v,tp)) = put_type(v,tp)
+  | string_of_combterm _ (CombVar(v,tp)) = put_type(v,tp)
+  | string_of_combterm is_pred (CombApp(t1,t2,tp)) = 
+    let val s1 = string_of_combterm is_pred t1
+	val s2 = string_of_combterm is_pred t2
 	val app = app_str ^ (ResClause.paren_pack [s1,s2])
     in
-	if tp = bool_tp then app else put_type(app,tp)
+	put_type(app,tp)
     end
-  | string_of_combterm (Bool(t)) = 
-    let val t' = string_of_combterm t
+  | string_of_combterm is_pred (Bool(t)) = 
+    let val t' = string_of_combterm false t
     in
-	bool_str ^ (ResClause.paren_pack [t'])
+	if is_pred then bool_str ^ (ResClause.paren_pack [t'])
+	else t'
     end
-  | string_of_combterm (Equal(t1,t2)) =
-    let val s1 = string_of_combterm t1
-	val s2 = string_of_combterm t2
+  | string_of_combterm _ (Equal(t1,t2)) =
+    let val s1 = string_of_combterm false t1
+	val s2 = string_of_combterm false t2
     in
 	"equal" ^ (ResClause.paren_pack [s1,s2]) 
     end;
@@ -398,7 +398,7 @@
 
 
 fun tptp_literal (Literal(pol,pred)) =
-    let val pred_string = string_of_combterm pred
+    let val pred_string = string_of_combterm true pred
 	val pol_str = if pol then "++" else "--"
     in
 	pol_str ^ pred_string