# HG changeset patch
# User mengj
# Date 1146196772 -7200
# Node ID cd6c71c57f5371166f5e1402718f1a61f0626cfe
# Parent  bf7f8347174a2dd9b0d5d9b848e60ad87c9de125
changed the functions for getting HOL helper clauses.

diff -r bf7f8347174a -r cd6c71c57f53 src/HOL/Tools/res_hol_clause.ML
--- a/src/HOL/Tools/res_hol_clause.ML	Fri Apr 28 05:58:53 2006 +0200
+++ b/src/HOL/Tools/res_hol_clause.ML	Fri Apr 28 05:59:32 2006 +0200
@@ -732,43 +732,31 @@
 (* write clauses to files                                             *)
 (**********************************************************************)
 
-fun read_in [] = []
-  | read_in (f1::fs) =
-    let val lines = read_in fs
-	val input = TextIO.openIn f1
-	fun reading () =
-	    let val nextline = TextIO.inputLine input
-	    in
-		if nextline = "" then (TextIO.closeIn input; [])
-		else nextline::(reading ())
-	    end
-    in
-	((reading ()) @ lines)
-    end;
+fun read_in fs = map (File.read o File.unpack_platform_path) fs; 
 
- 
-fun get_helper_clauses (full,partial,const,untyped) =
-    let val (helper1,noS,inclS) = case !typ_level of T_FULL => (warning "Fully-typed HOL"; full)
-						   | T_PARTIAL => (warning "Partially-typed HOL"; partial)
-						   | T_CONST => (warning "Const-only-typed HOL"; const)
-						   | T_NONE => (warning "Untyped HOL"; untyped)
-	val needed_helpers = if !include_combS then (warning "Include combinator S"; [helper1,inclS]) else
-			     if !include_min_comb then (warning "Include min combinators"; [helper1,noS])
-			     else (warning "No combinator is used"; [helper1])
+fun get_helper_clauses_tptp () =
+    let val tlevel = case !typ_level of T_FULL => (warning "Fully-typed HOL"; "~~/src/HOL/Tools/atp-inputs/full_")
+				      | T_PARTIAL => (warning "Partially-typed HOL"; "~~/src/HOL/Tools/atp-inputs/par_")
+				      | T_CONST => (warning "Const-only-typed HOL"; "~~/src/HOL/Tools/atp-inputs/const_")
+				      | T_NONE => (warning "Untyped HOL"; "~~/src/HOL/Tools/atp-inputs/u_")
+	val helpers = if !include_combS then (warning "Include combinator S"; ["helper1.tptp","comb_inclS.tptp"]) else
+		     if !include_min_comb then (warning "Include min combinators"; ["helper1.tptp","comb_noS.tptp"])
+		     else (warning "No combinator is used"; ["helper1.tptp"])
+	val t_helpers = map (curry (op ^) tlevel) helpers
     in
-	read_in needed_helpers
+	read_in t_helpers
     end;
-
-
+	
+						  
 (* write TPTP format to a single file *)
 (* when "get_helper_clauses" is called, "include_combS" and "include_min_comb" should have correct values already *)
-fun tptp_write_file thms filename (axclauses,classrel_clauses,arity_clauses) helpers =
+fun tptp_write_file thms filename (axclauses,classrel_clauses,arity_clauses) =
     let val clss = make_conjecture_clauses thms
 	val axclauses' = make_axiom_clauses axclauses
 	val (tptp_clss,tfree_litss) = ListPair.unzip (map clause2tptp clss)
 	val tfree_clss = map ResClause.tptp_tfree_clause (foldl (op union_string) [] tfree_litss)
 	val out = TextIO.openOut filename
-	val helper_clauses = get_helper_clauses helpers
+	val helper_clauses = get_helper_clauses_tptp ()
     in
 	List.app (curry TextIO.output out o #1 o clause2tptp) axclauses';
 	ResClause.writeln_strs out tfree_clss;