# HG changeset patch
# User paulson
# Date 1139484031 -3600
# Node ID 5060ca625e020193efd02922804af07349c2f4d6
# Parent  bc23b1d1ddea6c2d2448e3fa5d1f2bc82a27aeb8
tidying

diff -r bc23b1d1ddea -r 5060ca625e02 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Thu Feb 09 12:20:02 2006 +0100
+++ b/src/HOL/Tools/res_atp.ML	Thu Feb 09 12:20:31 2006 +0100
@@ -100,16 +100,21 @@
   end
 
 (*We write out problem files for each subgoal. Argument pf generates filenames,
-  and allows the suppression of the suffix "_1" in problem-generation mode.*)
+  and allows the suppression of the suffix "_1" in problem-generation mode.
+  FIXME: does not cope with &&, and it isn't easy because one could have multiple
+  subgoals, each involving &&.*)
 fun write_problem_files pf (ctxt,th)  =
   let val goals = Thm.prems_of th
+      val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals));
       val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt goals 
       val _ = Output.debug ("claset and simprules total clauses = " ^ 
                      Int.toString (Array.length clause_arr))
       val thy = ProofContext.theory_of ctxt
-      val classrel_clauses = if !ResClause.keep_types then ResClause.classrel_clauses_thy thy else []
+      val classrel_clauses = 
+          if !ResClause.keep_types then ResClause.classrel_clauses_thy thy else []
       val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
-      val arity_clauses = if !ResClause.keep_types then ResClause.arity_clause_thy thy else []
+      val arity_clauses = 
+          if !ResClause.keep_types then ResClause.arity_clause_thy thy else []
       val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
       val write = if !prover = "spass" then ResClause.dfg_write_file 
                                        else ResClause.tptp_write_file
@@ -174,7 +179,6 @@
     Output.debug ("subgoals in isar_atp:\n" ^ 
            Pretty.string_of (ProofContext.pretty_term ctxt
              (Logic.mk_conjunction_list (Thm.prems_of goal))));
-    Output.debug ("number of subgoals in isar_atp: " ^ Int.toString (Thm.nprems_of goal));
     Output.debug ("current theory: " ^ Context.theory_name thy);
     hook_count := !hook_count +1;
     Output.debug ("in hook for time: " ^ Int.toString (!hook_count));