1.1 --- a/src/HOL/Tools/res_atp.ML	Mon Jul 11 14:52:55 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Jul 11 16:42:42 2005 +0200
     1.3 @@ -113,7 +113,7 @@
     1.4  (* convert clauses from "assume" to conjecture. write to file "hyps" *)
     1.5  (* hypotheses of the goal currently being proved                     *)
     1.6  (*********************************************************************)
     1.7 -
     1.8 +(*perhaps have 2 different versions of this, depending on whether or not SpassComm.spass is set *)
     1.9  fun isar_atp_h thms =
    1.10          
    1.11      let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
    1.12 @@ -123,6 +123,7 @@
    1.13          val clss = map ResClause.make_conjecture_clause prems'''
    1.14  	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
    1.15  	val tfree_lits = ResLib.flat_noDup tfree_litss
    1.16 +        (* tfree clause is different in tptp and dfg versions *)
    1.17  	val tfree_clss = map ResClause.tfree_clause tfree_lits 
    1.18          val hypsfile = File.platform_path hyps_file
    1.19  	val out = TextIO.openOut(hypsfile)
    1.20 @@ -151,6 +152,24 @@
    1.21      end;
    1.22  
    1.23  
    1.24 +(*********************************************************************)
    1.25 +(* write out a subgoal as DFG clauses to the file "probN"           *)
    1.26 +(* where N is the number of this subgoal                             *)
    1.27 +(*********************************************************************)
    1.28 +(*
    1.29 +fun dfg_inputs_tfrees thms n tfrees = 
    1.30 +    let val _ = (warning ("in dfg_inputs_tfrees 0"))
    1.31 +        val clss = map (ResClause.make_conjecture_clause_thm) thms
    1.32 +         val _ = (warning ("in dfg_inputs_tfrees 1"))
    1.33 +	val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss)
    1.34 +        val _ = (warning ("in dfg_inputs_tfrees 2"))
    1.35 +	val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) 
    1.36 +         val _ = (warning ("in dfg_inputs_tfrees 3"))
    1.37 +        val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
    1.38 +	val out = TextIO.openOut(probfile)
    1.39 +    in
    1.40 +	(ResLib.writeln_strs out (tfree_clss @ dfg_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
    1.41 +    end;*)
    1.42  
    1.43  (*********************************************************************)
    1.44  (* call SPASS with settings and problem file for the current subgoal *)