src/HOL/Tools/res_atp.ML
changeset 17231 f42bc4f7afdf
parent 17150 ce2a1aeb42aa
child 17234 12a9393c5d77
     1.1 --- a/src/HOL/Tools/res_atp.ML	Fri Sep 02 15:25:27 2005 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Fri Sep 02 15:25:44 2005 +0200
     1.3 @@ -143,28 +143,18 @@
     1.4  (* where N is the number of this subgoal                             *)
     1.5  (*********************************************************************)
     1.6  
     1.7 -(*fun dfg_inputs_tfrees thms n tfrees axclauses= 
     1.8 -    let  val clss = map (ResClause.make_conjecture_clause_thm) thms
     1.9 -         val _ = (debug ("in dfg_inputs_tfrees 1"))
    1.10 -	 val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss)
    1.11 -	 val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) 
    1.12 -         val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
    1.13 -         val filestr = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) axclauses [] [] [] tfrees   
    1.14 -	 val out = TextIO.openOut(probfile)
    1.15 -    in
    1.16 -	(ResLib.writeln_strs out (tfree_clss @ dfg_clss); TextIO.closeOut out; debug probfile)
    1.17 -    end;
    1.18 -*)
    1.19  fun dfg_inputs_tfrees thms n tfrees axclauses = 
    1.20      let val clss = map (ResClause.make_conjecture_clause_thm) thms
    1.21          val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n)
    1.22 -        val _ = warning ("about to write out dfg prob file "^probfile)
    1.23 +        val _ = debug ("about to write out dfg prob file " ^ probfile)
    1.24         	(*val (dfg_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2dfg clss)
    1.25          val tfree_clss = map ResClause.tfree_dfg_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) *)   
    1.26 -        val filestr = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) axclauses [] [] [] tfrees   
    1.27 +        val filestr = ResClause.clauses2dfg clss ("prob" ^ (string_of_int n)) 
    1.28 +                        axclauses [] [] [] tfrees   
    1.29  	val out = TextIO.openOut(probfile)
    1.30      in
    1.31  	(ResLib.writeln_strs out [filestr]; TextIO.closeOut out; debug probfile )
    1.32 +(* (ResLib.writeln_strs out (tfree_clss @ dfg_clss); *)
    1.33      end;
    1.34  
    1.35  
    1.36 @@ -238,11 +228,13 @@
    1.37  	
    1.38       ( SELECT_GOAL
    1.39          (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    1.40 -          METAHYPS(fn negs => (if !SpassComm.spass then 
    1.41 -				    dfg_inputs_tfrees (make_clauses negs) n tfrees axclauses
    1.42 - 				 else
    1.43 -			  	    tptp_inputs_tfrees (make_clauses negs)  n tfrees;
    1.44 -			            get_sko_thms  tfrees sign sg_terms (childin, childout, pid) thm  (n -1) (negs::sko_thms) axclauses; dummy_tac))]) n thm )
    1.45 +          METAHYPS(fn negs => 
    1.46 +            (if !SpassComm.spass 
    1.47 +             then dfg_inputs_tfrees (make_clauses negs) n tfrees axclauses
    1.48 +             else tptp_inputs_tfrees (make_clauses negs) n tfrees;
    1.49 +             get_sko_thms tfrees sign sg_terms (childin, childout, pid) 
    1.50 +                          thm  (n -1) (negs::sko_thms) axclauses; 
    1.51 +             dummy_tac))]) n thm )
    1.52  
    1.53  
    1.54  
    1.55 @@ -277,7 +269,7 @@
    1.56  (* write to file "hyps"                           *)
    1.57  (**************************************************)
    1.58  
    1.59 -fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid)  axclauses=
    1.60 +fun isar_atp_aux thms thm n_subgoals  (childin, childout, pid) axclauses =
    1.61    let val tfree_lits = isar_atp_h thms
    1.62    in
    1.63      debug ("in isar_atp_aux");