removing the string array from the result of get_clasimp_atp_lemmas
authorpaulson
Wed May 17 12:28:47 2006 +0200 (2006-05-17 ago)
changeset 19675a4894fb2a5f2
parent 19674 22b635240905
child 19676 187234ec6050
removing the string array from the result of get_clasimp_atp_lemmas
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Wed May 17 01:23:48 2006 +0200
     1.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Wed May 17 12:28:47 2006 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4        Proof.context ->
     1.5        Term.term list ->
     1.6        (string * Thm.thm) list ->
     1.7 -      (bool * bool * bool) -> bool -> string Array.array * (thm * (string * int)) list
     1.8 +      (bool * bool * bool) -> bool -> (thm * (string * int)) list
     1.9    end;
    1.10    
    1.11  structure ResClasimp : RES_CLASIMP =
    1.12 @@ -281,10 +281,12 @@
    1.13  	  if run_filter 
    1.14  	  then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals
    1.15  	  else cls_thms_list
    1.16 -      val all_relevant_cls_thms_list = insert_thms (List.concat user_cls_thms) relevant_cls_thms_list (*ensure all user supplied rules are output*)	  
    1.17 +      val all_relevant_cls_thms_list = 
    1.18 +            insert_thms (List.concat user_cls_thms) relevant_cls_thms_list 
    1.19 +            (*ensure all user supplied rules are output*)
    1.20      in
    1.21 -	(Array.fromList (map fst (map snd all_relevant_cls_thms_list)), all_relevant_cls_thms_list)
    1.22 -end;
    1.23 +	all_relevant_cls_thms_list
    1.24 +    end;
    1.25  
    1.26  
    1.27  	
     2.1 --- a/src/HOL/Tools/res_atp.ML	Wed May 17 01:23:48 2006 +0200
     2.2 +++ b/src/HOL/Tools/res_atp.ML	Wed May 17 12:28:47 2006 +0200
     2.3 @@ -304,7 +304,7 @@
     2.4  	val hyp_cls = cnf_hyps_thms ctxt
     2.5  	val goal_cls = conj_cls@hyp_cls
     2.6  	val user_rules = map ResAxioms.pairname user_thms
     2.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)  
     2.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)  
     2.9  	val thy = ProofContext.theory_of ctxt
    2.10  	val prob_logic = case mode of Auto => problem_logic_goals [map prop_of goal_cls]
    2.11  				    | Fol => FOL
    2.12 @@ -398,9 +398,9 @@
    2.13  fun write_problem_files pf (ctxt,th)  =
    2.14    let val goals = Thm.prems_of th
    2.15        val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
    2.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 *)
    2.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 *)
    2.18        val _ = Output.debug ("claset, simprules and atprules total clauses = " ^ 
    2.19 -                     Int.toString (Array.length names_arr))
    2.20 +                     Int.toString (length axclauses))
    2.21        val thy = ProofContext.theory_of ctxt
    2.22        fun get_neg_subgoals n =
    2.23  	  if n=0 then []
    2.24 @@ -425,8 +425,9 @@
    2.25        fun write_all [] _ = []
    2.26  	| write_all (subgoal::subgoals) k =
    2.27  	  (writer goals_logic subgoal (pf k) (axclauses,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1))
    2.28 +      val thm_names = Array.fromList (map (#1 o #2) axclauses)
    2.29    in
    2.30 -      (write_all neg_subgoals (length goals), names_arr)
    2.31 +      (write_all neg_subgoals (length goals), thm_names)
    2.32    end;
    2.33  
    2.34  val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
    2.35 @@ -449,8 +450,8 @@
    2.36    else
    2.37      let
    2.38        val _ = kill_last_watcher()
    2.39 -      val (files,names_arr) = write_problem_files prob_pathname (ctxt,th)
    2.40 -      val (childin, childout, pid) = Watcher.createWatcher (th, names_arr)
    2.41 +      val (files,thm_names) = write_problem_files prob_pathname (ctxt,th)
    2.42 +      val (childin, childout, pid) = Watcher.createWatcher (th, thm_names)
    2.43      in
    2.44        last_watcher_pid := SOME (childin, childout, pid, files);
    2.45        Output.debug ("problem files: " ^ space_implode ", " files);