src/HOL/Tools/res_atp.ML

 
 (*********************************************************************)
 (* convert clauses from "assume" to conjecture. write to file "hyps" *)
 (* hypotheses of the goal currently being proved                     *)
 (*********************************************************************)
-
+(*perhaps have 2 different versions of this, depending on whether or not SpassComm.spass is set *)
 fun isar_atp_h thms =
         
     let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
         val prems' = map repeat_someI_ex prems
         val prems'' = make_clauses prems'
         val prems''' = ResAxioms.rm_Eps [] prems''
         val clss = map ResClause.make_conjecture_clause prems'''
 	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
 	val tfree_lits = ResLib.flat_noDup tfree_litss
+        (* tfree clause is different in tptp and dfg versions *)
 	val tfree_clss = map ResClause.tfree_clause tfree_lits 
         val hypsfile = File.platform_path hyps_file
 	val out = TextIO.openOut(hypsfile)
     in
 	((ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; if !trace_res then (warning hypsfile) else ());tfree_lits) 

     in
 	(ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
     end;
 
 
+(*********************************************************************)
+(* write out a subgoal as DFG clauses to the file "probN"           *)
+(* where N is the number of this subgoal                             *)
+(*********************************************************************)
+(*
+fun dfg_inputs_tfrees thms n tfrees = 
+    let val _ = (warning ("in dfg_inputs_tfrees 0"))
+        val clss = map (ResClause.make_conjecture_clause_thm) thms
+         val _ = (warning ("in dfg_inputs_tfrees 1"))
+	val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss)
+        val _ = (warning ("in dfg_inputs_tfrees 2"))
+	val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) 
+         val _ = (warning ("in dfg_inputs_tfrees 3"))
+        val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
+	val out = TextIO.openOut(probfile)
+    in
+	(ResLib.writeln_strs out (tfree_clss @ dfg_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
+    end;*)
 
 (*********************************************************************)
 (* call SPASS with settings and problem file for the current subgoal *)
 (* should be modified to allow other provers to be called            *)
 (*********************************************************************)