src/HOL/Tools/res_atp.ML
changeset 18986 5060ca625e02
parent 18863 a113b6839df1
child 19194 7681c04d8bff
     1.1 --- a/src/HOL/Tools/res_atp.ML	Thu Feb 09 12:20:02 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Feb 09 12:20:31 2006 +0100
     1.3 @@ -100,16 +100,21 @@
     1.4    end
     1.5  
     1.6  (*We write out problem files for each subgoal. Argument pf generates filenames,
     1.7 -  and allows the suppression of the suffix "_1" in problem-generation mode.*)
     1.8 +  and allows the suppression of the suffix "_1" in problem-generation mode.
     1.9 +  FIXME: does not cope with &&, and it isn't easy because one could have multiple
    1.10 +  subgoals, each involving &&.*)
    1.11  fun write_problem_files pf (ctxt,th)  =
    1.12    let val goals = Thm.prems_of th
    1.13 +      val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals));
    1.14        val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt goals 
    1.15        val _ = Output.debug ("claset and simprules total clauses = " ^ 
    1.16                       Int.toString (Array.length clause_arr))
    1.17        val thy = ProofContext.theory_of ctxt
    1.18 -      val classrel_clauses = if !ResClause.keep_types then ResClause.classrel_clauses_thy thy else []
    1.19 +      val classrel_clauses = 
    1.20 +          if !ResClause.keep_types then ResClause.classrel_clauses_thy thy else []
    1.21        val _ = Output.debug ("classrel clauses = " ^ Int.toString (length classrel_clauses))
    1.22 -      val arity_clauses = if !ResClause.keep_types then ResClause.arity_clause_thy thy else []
    1.23 +      val arity_clauses = 
    1.24 +          if !ResClause.keep_types then ResClause.arity_clause_thy thy else []
    1.25        val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
    1.26        val write = if !prover = "spass" then ResClause.dfg_write_file 
    1.27                                         else ResClause.tptp_write_file
    1.28 @@ -174,7 +179,6 @@
    1.29      Output.debug ("subgoals in isar_atp:\n" ^ 
    1.30             Pretty.string_of (ProofContext.pretty_term ctxt
    1.31               (Logic.mk_conjunction_list (Thm.prems_of goal))));
    1.32 -    Output.debug ("number of subgoals in isar_atp: " ^ Int.toString (Thm.nprems_of goal));
    1.33      Output.debug ("current theory: " ^ Context.theory_name thy);
    1.34      hook_count := !hook_count +1;
    1.35      Output.debug ("in hook for time: " ^ Int.toString (!hook_count));