src/HOL/Tools/res_atp.ML
changeset 18753 aa82bd41555d
parent 18700 f04a8755d6ca
child 18798 ca02a2077955
     1.1 --- a/src/HOL/Tools/res_atp.ML	Mon Jan 23 11:38:43 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Mon Jan 23 11:41:54 2006 +0100
     1.3 @@ -136,9 +136,8 @@
     1.4  (*We write out problem files for each subgoal. Argument pf generates filenames,
     1.5    and allows the suppression of the suffix "_1" in problem-generation mode.*)
     1.6  fun write_problem_files pf (ctxt,th)  =
     1.7 -  let val prems = Thm.prems_of th
     1.8 -      val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt (hd prems) 
     1.9 -              (*FIXME: hack!! need to consider relevance for all prems*)
    1.10 +  let val goals = Thm.prems_of th
    1.11 +      val (clause_arr, axclauses) = ResClasimp.get_clasimp_lemmas ctxt goals 
    1.12        val _ = Output.debug ("claset and simprules total clauses = " ^ 
    1.13                       Int.toString (Array.length clause_arr))
    1.14        val thy = ProofContext.theory_of ctxt
    1.15 @@ -157,7 +156,7 @@
    1.16  		       (axclauses,classrel_clauses,arity_clauses);
    1.17  		 all_tac))]) n th;
    1.18  	    pf n :: writenext (n-1))
    1.19 -      in (writenext (length prems), clause_arr) end;
    1.20 +      in (writenext (length goals), clause_arr) end;
    1.21  
    1.22  val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
    1.23                                      Posix.Process.pid * string list) option);