src/HOL/Tools/res_atp.ML
changeset 19675 a4894fb2a5f2
parent 19641 f1de44e61ec1
child 19718 e709f643c578
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed May 17 01:23:48 2006 +0200
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed May 17 12:28:47 2006 +0200
     1.3 @@ -304,7 +304,7 @@
     1.4  	val hyp_cls = cnf_hyps_thms ctxt
     1.5  	val goal_cls = conj_cls@hyp_cls
     1.6  	val user_rules = map ResAxioms.pairname user_thms
     1.7 -	val (names_arr,axclauses_as_thms) = ResClasimp.get_clasimp_atp_lemmas ctxt (map prop_of goal_cls) user_rules (!include_claset,!include_simpset,!include_atpset) (!run_relevance_filter)  
     1.8 +	val axclauses_as_thms = ResClasimp.get_clasimp_atp_lemmas ctxt (map prop_of goal_cls) user_rules (!include_claset,!include_simpset,!include_atpset) (!run_relevance_filter)  
     1.9  	val thy = ProofContext.theory_of ctxt
    1.10  	val prob_logic = case mode of Auto => problem_logic_goals [map prop_of goal_cls]
    1.11  				    | Fol => FOL
    1.12 @@ -398,9 +398,9 @@
    1.13  fun write_problem_files pf (ctxt,th)  =
    1.14    let val goals = Thm.prems_of th
    1.15        val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
    1.16 -      val (names_arr, axclauses) = ResClasimp.get_clasimp_atp_lemmas ctxt goals [] (true,true,true) (!run_relevance_filter) (* no user supplied rules here, because no user invocation *)
    1.17 +      val axclauses = ResClasimp.get_clasimp_atp_lemmas ctxt goals [] (true,true,true) (!run_relevance_filter) (* no user supplied rules here, because no user invocation *)
    1.18        val _ = Output.debug ("claset, simprules and atprules total clauses = " ^ 
    1.19 -                     Int.toString (Array.length names_arr))
    1.20 +                     Int.toString (length axclauses))
    1.21        val thy = ProofContext.theory_of ctxt
    1.22        fun get_neg_subgoals n =
    1.23  	  if n=0 then []
    1.24 @@ -425,8 +425,9 @@
    1.25        fun write_all [] _ = []
    1.26  	| write_all (subgoal::subgoals) k =
    1.27  	  (writer goals_logic subgoal (pf k) (axclauses,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1))
    1.28 +      val thm_names = Array.fromList (map (#1 o #2) axclauses)
    1.29    in
    1.30 -      (write_all neg_subgoals (length goals), names_arr)
    1.31 +      (write_all neg_subgoals (length goals), thm_names)
    1.32    end;
    1.33  
    1.34  val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
    1.35 @@ -449,8 +450,8 @@
    1.36    else
    1.37      let
    1.38        val _ = kill_last_watcher()
    1.39 -      val (files,names_arr) = write_problem_files prob_pathname (ctxt,th)
    1.40 -      val (childin, childout, pid) = Watcher.createWatcher (th, names_arr)
    1.41 +      val (files,thm_names) = write_problem_files prob_pathname (ctxt,th)
    1.42 +      val (childin, childout, pid) = Watcher.createWatcher (th, thm_names)
    1.43      in
    1.44        last_watcher_pid := SOME (childin, childout, pid, files);
    1.45        Output.debug ("problem files: " ^ space_implode ", " files);