# HG changeset patch
# User paulson
# Date 1147861727 -7200
# Node ID a4894fb2a5f2e8601695ead25f31df4b2e5750d6
# Parent  22b63524090590c95a5298864a92b2a7e5af97b2
removing the string array from the result of get_clasimp_atp_lemmas

diff -r 22b635240905 -r a4894fb2a5f2 src/HOL/Tools/ATP/res_clasimpset.ML
--- a/src/HOL/Tools/ATP/res_clasimpset.ML	Wed May 17 01:23:48 2006 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Wed May 17 12:28:47 2006 +0200
@@ -12,7 +12,7 @@
       Proof.context ->
       Term.term list ->
       (string * Thm.thm) list ->
-      (bool * bool * bool) -> bool -> string Array.array * (thm * (string * int)) list
+      (bool * bool * bool) -> bool -> (thm * (string * int)) list
   end;
   
 structure ResClasimp : RES_CLASIMP =
@@ -281,10 +281,12 @@
 	  if run_filter 
 	  then ReduceAxiomsN.relevance_filter (ProofContext.theory_of ctxt) cls_thms_list goals
 	  else cls_thms_list
-      val all_relevant_cls_thms_list = insert_thms (List.concat user_cls_thms) relevant_cls_thms_list (*ensure all user supplied rules are output*)	  
+      val all_relevant_cls_thms_list = 
+            insert_thms (List.concat user_cls_thms) relevant_cls_thms_list 
+            (*ensure all user supplied rules are output*)
     in
-	(Array.fromList (map fst (map snd all_relevant_cls_thms_list)), all_relevant_cls_thms_list)
-end;
+	all_relevant_cls_thms_list
+    end;
 
 
 	
diff -r 22b635240905 -r a4894fb2a5f2 src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Wed May 17 01:23:48 2006 +0200
+++ b/src/HOL/Tools/res_atp.ML	Wed May 17 12:28:47 2006 +0200
@@ -304,7 +304,7 @@
 	val hyp_cls = cnf_hyps_thms ctxt
 	val goal_cls = conj_cls@hyp_cls
 	val user_rules = map ResAxioms.pairname user_thms
-	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)  
+	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)  
 	val thy = ProofContext.theory_of ctxt
 	val prob_logic = case mode of Auto => problem_logic_goals [map prop_of goal_cls]
 				    | Fol => FOL
@@ -398,9 +398,9 @@
 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 (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 *)
+      val axclauses = ResClasimp.get_clasimp_atp_lemmas ctxt goals [] (true,true,true) (!run_relevance_filter) (* no user supplied rules here, because no user invocation *)
       val _ = Output.debug ("claset, simprules and atprules total clauses = " ^ 
-                     Int.toString (Array.length names_arr))
+                     Int.toString (length axclauses))
       val thy = ProofContext.theory_of ctxt
       fun get_neg_subgoals n =
 	  if n=0 then []
@@ -425,8 +425,9 @@
       fun write_all [] _ = []
 	| write_all (subgoal::subgoals) k =
 	  (writer goals_logic subgoal (pf k) (axclauses,classrel_clauses,arity_clauses); pf k):: (write_all subgoals (k - 1))
+      val thm_names = Array.fromList (map (#1 o #2) axclauses)
   in
-      (write_all neg_subgoals (length goals), names_arr)
+      (write_all neg_subgoals (length goals), thm_names)
   end;
 
 val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
@@ -449,8 +450,8 @@
   else
     let
       val _ = kill_last_watcher()
-      val (files,names_arr) = write_problem_files prob_pathname (ctxt,th)
-      val (childin, childout, pid) = Watcher.createWatcher (th, names_arr)
+      val (files,thm_names) = write_problem_files prob_pathname (ctxt,th)
+      val (childin, childout, pid) = Watcher.createWatcher (th, thm_names)
     in
       last_watcher_pid := SOME (childin, childout, pid, files);
       Output.debug ("problem files: " ^ space_implode ", " files);