src/HOL/Tools/res_atp.ML
changeset 19718 e709f643c578
parent 19675 a4894fb2a5f2
child 19722 e7a5b54248bc
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu May 25 08:07:02 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu May 25 08:08:04 2006 +0200
     1.3 @@ -291,12 +291,10 @@
     1.4      then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
     1.5      else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities);
     1.6  
     1.7 -(*2006-04-07: not working: goals has type thm list (not term list as above) and
     1.8 -  axioms has type ResClause.clause list (not (thm * (string * int)) list as above)*)
     1.9  fun dfg_writer logic goals filename (axioms,classrels,arities) =
    1.10      if is_fol_logic logic 
    1.11      then ResClause.dfg_write_file goals filename (axioms, classrels, arities)
    1.12 -    else error "DFG output for higher-order translations is not implemented"
    1.13 +    else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities);
    1.14  
    1.15  
    1.16  fun write_subgoal_file mode ctxt conjectures user_thms n =
    1.17 @@ -312,7 +310,7 @@
    1.18  	val keep_types = if is_fol_logic prob_logic then !fol_keep_types else is_typed_hol ()
    1.19  	val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
    1.20  	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
    1.21 -        val writer = (*if !prover = "spass" then dfg_writer else*) tptp_writer 
    1.22 +        val writer = if !prover = "spass" then dfg_writer else tptp_writer 
    1.23  	val file = atp_input_file()
    1.24      in
    1.25  	(writer prob_logic goal_cls file (axclauses_as_thms,classrel_clauses,arity_clauses);
    1.26 @@ -421,7 +419,7 @@
    1.27        val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
    1.28        val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
    1.29        val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
    1.30 -      val writer = (*if !prover = "spass" then dfg_writer else*) tptp_writer 
    1.31 +      val writer = if !prover = "spass" then dfg_writer else tptp_writer 
    1.32        fun write_all [] _ = []
    1.33  	| write_all (subgoal::subgoals) k =
    1.34  	  (writer goals_logic subgoal (pf k) (axclauses,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1))