Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
Changed watcher.ML so that the Unix.execute and Unix.reap functions are used instead of those in modUnix.ML, and
consequently removed modUnix.ML from Reconstruction.thy

--- a/src/HOL/Reconstruction.thy	Sun May 22 19:26:18 2005 +0200
+++ b/src/HOL/Reconstruction.thy	Mon May 23 00:18:51 2005 +0200
@@ -21,7 +21,7 @@
  	  "Tools/ATP/recon_transfer_proof.ML"
 	  "Tools/ATP/VampireCommunication.ML"
 	  "Tools/ATP/SpassCommunication.ML"
-	  "Tools/ATP/modUnix.ML"
+	 (* "Tools/ATP/modUnix.ML"**)
 	  "Tools/ATP/watcher.sig"
 	  "Tools/ATP/watcher.ML"
 	  "Tools/ATP/res_clasimpset.ML"

--- a/src/HOL/Tools/ATP/modUnix.ML	Sun May 22 19:26:18 2005 +0200
+++ b/src/HOL/Tools/ATP/modUnix.ML	Mon May 23 00:18:51 2005 +0200
@@ -7,6 +7,10 @@
 (****** Slightly modified version of sml Unix structure *********)
 (****************************************************************)
 
+
+structure modUnix: MODUNIX =
+  struct
+
 type signal = Posix.Signal.signal
 datatype exit_status = datatype Posix.Process.exit_status
 
@@ -272,3 +276,5 @@
               outstr = outstr
             })::procList))
           end;
+
+end;

--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Sun May 22 19:26:18 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon May 23 00:18:51 2005 +0200
@@ -453,6 +453,10 @@
                                               in 
                                                   TextIO.output (toParent,"Proof found but translation failed!" ^"\n");
                                                   TextIO.flushOut toParent;
+						TextIO.output (toParent, thmstring^"\n");
+                                         	   TextIO.flushOut toParent;
+                                         	   TextIO.output (toParent, goalstring^"\n");
+                                         	   TextIO.flushOut toParent;
             					  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
                                          	  (* Attempt to prevent several signals from turning up simultaneously *)
                                          	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac

--- a/src/HOL/Tools/ATP/res_clasimpset.ML	Sun May 22 19:26:18 2005 +0200
+++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Mon May 23 00:18:51 2005 +0200
@@ -1,4 +1,6 @@
+
 (*  ID:         $Id$
+
     Author:     Claire Quigley
     Copyright   2004  University of Cambridge
 *)
@@ -10,32 +12,56 @@
 
 structure ResClasimp : RES_CLASIMP =
 struct
-
+fun has_name th = not((Thm.name_of_thm th )= "")
 fun has_name_pair (a,b) = not_equal a "";
 
 fun stick []  = []
 |   stick (x::xs)  = x@(stick xs )
 
+fun filterlist p [] = []
+|   filterlist p (x::xs) = if p x 
+                           then 
+                               (x::(filterlist p xs))
+                           else
+                               filterlist p xs
+
+
 (* changed, now it also finds out the name of the theorem. *)
 (* convert a theorem into CNF and then into Clause.clause format. *)
-fun clausify_axiom_pairs thm =
-    let val thm_name = Thm.name_of_thm thm
-	val isa_clauses = ResAxioms.cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *)
-        val isa_clauses' = ResAxioms.rm_Eps [] isa_clauses
-        val clauses_n = length isa_clauses
-	fun make_axiom_clauses _ [] []= []
-	  | make_axiom_clauses i (cls::clss) (cls'::clss')= ((ResClause.make_axiom_clause cls (thm_name,i)),cls') :: make_axiom_clauses (i+1) clss clss'
-    in
-	make_axiom_clauses 0 isa_clauses' isa_clauses		
-    end;
+
+(* outputs a list of (thm,clause) pairs *)
 
 
-fun clausify_rules_pairs [] err_list = ([],err_list)
-  | clausify_rules_pairs (thm::thms) err_list =
-    let val (ts,es) = clausify_rules_pairs thms err_list
-    in
-	((clausify_axiom_pairs thm)::ts,es) handle  _ => (ts,(thm::es))
-    end;
+(* for tracing: encloses each string element in brackets. *)
+fun concat_with_stop [] = ""
+  | concat_with_stop [x] =  x
+  | concat_with_stop (x::xs) = x^ "." ^ concat_with_stop xs;
+
+fun remove_symb str = if String.isPrefix  "List.op @." str
+                      then 
+                          ((String.substring(str,0,5))^(String.extract (str, 10, NONE)))
+                      else
+                          str
+
+fun remove_spaces str = let val strlist = String.tokens Char.isSpace str
+                            val spaceless = concat strlist
+                            val strlist' = String.tokens Char.isPunct spaceless
+                        in
+                            concat_with_stop strlist'
+                        end
+
+fun remove_symb_pair (str, thm) = let val newstr = remove_symb str
+                                  in
+                                    (newstr, thm)
+                                  end
+
+
+fun remove_spaces_pair (str, thm) = let val newstr = remove_spaces str
+                                  in
+                                    (newstr, thm)
+                                  end
+
+
 
 
 (*Insert th into the result provided the name is not "".*)
@@ -44,12 +70,14 @@
 
 fun write_out_clasimp filename = let
 					val claset_rules = ResAxioms.claset_rules_of_thy (the_context());
-					val named_claset = List.foldr add_nonempty []  claset_rules;
-					val claset_cls_thms = #1( clausify_rules_pairs named_claset []);
+					val named_claset = filterlist has_name_pair claset_rules;
+					val claset_names = map remove_spaces_pair (named_claset)
+					val claset_cls_thms = #1( ResAxioms.clausify_rules_pairs named_claset []);
+
 
 					val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context());
-					val named_simpset = map #2(List.filter has_name_pair simpset_rules);
-					val simpset_cls_thms = #1 (clausify_rules_pairs named_simpset []);
+					val named_simpset = map remove_spaces_pair (filterlist has_name_pair simpset_rules);
+					val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
 
 					val cls_thms = (claset_cls_thms@simpset_cls_thms);
 					val cls_thms_list = stick cls_thms;
@@ -79,3 +107,4 @@
 
 
 end;
+

--- a/src/HOL/Tools/ATP/watcher.ML	Sun May 22 19:26:18 2005 +0200
+++ b/src/HOL/Tools/ATP/watcher.ML	Mon May 23 00:18:51 2005 +0200
@@ -25,7 +25,90 @@
 
 val goals_being_watched = ref 0;
 
+(*****************************************)
+(*  The result of calling createWatcher  *)
+(*****************************************)
 
+datatype proc = PROC of {
+        pid : Posix.Process.pid,
+        instr : TextIO.instream,
+        outstr : TextIO.outstream
+      };
+
+(*****************************************)
+(*  The result of calling executeToList  *)
+(*****************************************)
+
+datatype cmdproc = CMDPROC of {
+        prover: string,             (* Name of the resolution prover used, e.g. Vampire, SPASS *)
+        cmd:  string,              (* The file containing the goal for res prover to prove *)     
+        thmstring: string,         (* string representation of subgoal after negation, skolemization*) 
+        goalstring: string,         (* string representation of subgoal*) 
+        proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
+        instr : TextIO.instream,   (*  Input stream to child process *)
+        outstr : TextIO.outstream  (*  Output stream from child process *)
+      };
+
+type signal = Posix.Signal.signal
+datatype exit_status = datatype Posix.Process.exit_status
+
+val fromStatus = Posix.Process.fromStatus
+
+
+fun reap(pid, instr, outstr) =
+        let
+		val u = TextIO.closeIn instr;
+	        val u = TextIO.closeOut outstr;
+	
+		val (_, status) =
+			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
+	in
+		status
+	end
+
+fun fdReader (name : string, fd : Posix.IO.file_desc) =
+	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
+
+fun fdWriter (name, fd) =
+          Posix.IO.mkTextWriter {
+	      appendMode = false,
+              initBlkMode = true,
+              name = name,  
+              chunkSize=4096,
+              fd = fd
+            };
+
+fun openOutFD (name, fd) =
+	  TextIO.mkOutstream (
+	    TextIO.StreamIO.mkOutstream (
+	      fdWriter (name, fd), IO.BLOCK_BUF));
+
+fun openInFD (name, fd) =
+	  TextIO.mkInstream (
+	    TextIO.StreamIO.mkInstream (
+	      fdReader (name, fd), ""));
+
+
+
+
+
+fun killChild child_handle = Unix.reap child_handle 
+
+fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr));
+
+fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
+
+fun cmdInStream (CMDPROC{instr,outstr,...}) = (instr);
+
+fun cmdchildInfo (CMDPROC{prover,cmd,thmstring,proc_handle,goalstring,instr,outstr}) = (prover,(cmd, (instr,outstr)));
+
+fun cmdchildHandle (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = proc_handle;
+
+fun cmdProver (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (prover);
+
+fun cmdThm (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (thmstring);
+
+fun cmdGoal (CMDPROC{prover,cmd,thmstring,goalstring,proc_handle,instr,outstr})  = (goalstring);
 
 fun sendOutput (outstr,str) = (TextIO.outputSubstr (outstr, (Substring.all str));TextIO.flushOut outstr);
 
@@ -92,7 +175,7 @@
                                                          val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
                                                          (*** only include problem and clasimp for the moment, not sure how to refer to ***)
                                                          (*** hyps/local axioms just now                                                ***)
-                                                         val whole_prob_file = Unix.execute("/bin/cat", [(*clasimpfile,axfile, hypsfile,*)probfile,  ">", (File.sysify_path wholefile)])
+                                                         val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile,  ">", (File.sysify_path wholefile)])
                                                          val dfg_create =if File.exists dfg_dir 
                                                                          then
                                                                              ((warning("dfg dir exists"));())
@@ -100,8 +183,7 @@
                                                                                File.mkdir dfg_dir; 
                                                          
                                                          val dfg_path = File.sysify_path dfg_dir;
-                                                         val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X",
-                                                                                       ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path])
+                                                         val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X",   ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path])
                                                        (*val _ = Posix.Process.wait ()*)
                                                        (*val _ =Unix.reap exec_tptp2x*)
                                                          val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
@@ -289,7 +371,7 @@
                       val _ = TextIO.output (outfile,goalstr )
                       val _ =  TextIO.closeOut outfile*)
                       fun killChildren [] = ()
-                   |      killChildren  (childPid::children) = (killChild childPid; killChildren children)
+                   |      killChildren  (child_handle::children) = (killChild child_handle; killChildren children)
 
                      
            
@@ -356,7 +438,7 @@
                                                               (*********************************)
                     |   checkChildren ((childProc::otherChildren), toParentStr) = 
                                             let val (childInput,childOutput) =  cmdstreamsOf childProc
-                                                val childPid = cmdchildPid childProc
+                                                val child_handle= cmdchildHandle childProc
                                                 (* childCmd is the .dfg file that the problem is in *)
                                                 val childCmd = fst(snd (cmdchildInfo childProc))
                                                 (* now get the number of the subgoal from the filename *)
@@ -392,7 +474,7 @@
                                                        (**********************************************)
                                                        (* Remove this child and go on to check others*)
                                                        (**********************************************)
-                                                       ( reap(childPid, childInput, childOutput);
+                                                       ( Unix.reap child_handle;
                                                          checkChildren(otherChildren, toParentStr))
                                                     else 
                                                        (**********************************************)
@@ -418,35 +500,58 @@
                 (* takes list of (string, string, string list, string)list proclist *)
                 (********************************************************************)
 
-           (*** add subgoal id num to this *)
+
+  (*** add subgoal id num to this *)
                    fun execCmds  [] procList = procList
                    |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  = 
                                                      if (prover = "spass") 
                                                      then 
-                                                         let val newProcList = myexecuteToList (proverCmd,([prover]@[thmstring]@[goalstring]@["-FullRed=0"]@settings@[file]), procList)
+                                                         let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
+ 						             val (instr, outstr)=Unix.streamsOf childhandle
+                                                             val newProcList =    (((CMDPROC{
+            									  prover = prover,
+   										  cmd = file,
+  									          thmstring = thmstring,
+  									          goalstring = goalstring,
+ 										  proc_handle = childhandle,
+									          instr = instr,
+   									          outstr = outstr })::procList))
+  	                                                      val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "exec_child")));  
+                                                val _ = TextIO.output (outfile,"executing command for goal:"^goalstring^proverCmd^(concat settings)^file )
+                                                val _ =  TextIO.closeOut outfile
                                                          in
                                                             execCmds cmds newProcList
                                                          end
                                                      else 
-                                                         let val newProcList = myexecuteToList (proverCmd,([prover]@[thmstring]@[goalstring]@settings@[file]), procList)
+                                                         let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
+ 						             val (instr, outstr)=Unix.streamsOf childhandle
+							     val newProcList =    (((CMDPROC{
+            									  prover = prover,
+   										  cmd = file,
+  									          thmstring = thmstring,
+  									          goalstring = goalstring,
+ 										  proc_handle = childhandle,
+									          instr = instr,
+   									          outstr = outstr })::procList))
                                                          in
                                                             execCmds cmds newProcList
                                                          end
 
 
+
                 (****************************************)                  
                 (* call resolution processes remotely   *)
                 (* settings should be a list of strings *)
                 (* e.g. ["-t 300", "-m 100000"]         *)
                 (****************************************)
   
-                   fun execRemoteCmds  [] procList = procList
+                 (*  fun execRemoteCmds  [] procList = procList
                    |   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
                                              let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
                                                  in
                                                       execRemoteCmds  cmds newProcList
                                                  end
-
+*)
 
                    fun printList (outStr, []) = ()
                    |   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
@@ -463,9 +568,9 @@
                           let    fun loop (procList) =  
                                  (
                                  let val cmdsFromIsa = pollParentInput ()
-                                      fun killchildHandler (n:int)  = (TextIO.output(toParentStr, "Killing child proof processes!\n");
+                                     fun killchildHandler (n:int)  = (TextIO.output(toParentStr, "Killing child proof processes!\n");
                                                   TextIO.flushOut toParentStr;
-                                                   killChildren (map (cmdchildPid) procList);
+                                                   killChildren (map (cmdchildHandle) procList);
                                                     ())
                                      
                                  in 
@@ -476,11 +581,12 @@
                                           if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
                                           then 
                                             (
-                                              let val childPids = map cmdchildPid procList 
+                                              let val child_handles = map cmdchildHandle procList 
                                               in
-                                                 killChildren childPids;
-                                                 (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)                                       loop ([])
+                                                 killChildren child_handles;
+                                                 (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)                                                              loop ([])
                                               end
+                                                 
                                              )
                                           else
                                             ( 
@@ -496,11 +602,12 @@
                                                     loop (newProcList') 
                                                   end
                                                   )
-                                              else                         (************************)
-                                                                           (* Execute remotely     *)
-                                                  (                        (************************)
+                                              else                         (*********************************)
+                                                                           (* Execute remotely              *)
+ 									   (* (actually not remote for now )*)
+                                                  (                        (*********************************)
                                                   let 
-                                                    val newProcList = execRemoteCmds (valOf cmdsFromIsa) procList
+                                                    val newProcList = execCmds (valOf cmdsFromIsa) procList
                                                     val parentID = Posix.ProcEnv.getppid()
                                                     val newProcList' =checkChildren (newProcList, toParentStr) 
                                                   in
@@ -594,7 +701,19 @@
 (**********************************************************)
 (* Start a watcher and set up signal handlers             *)
 (**********************************************************)
-fun killWatcher pid= killChild pid;
+
+fun killWatcher pid= Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
+
+fun reapWatcher(pid, instr, outstr) =
+        let
+		val u = TextIO.closeIn instr;
+	        val u = TextIO.closeOut outstr;
+	
+		val (_, status) =
+			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
+	in
+		status
+	end
 
 fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
 			   val streams =snd mychild
@@ -636,7 +755,7 @@
                                                                          val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
                                                                          val _ =  TextIO.closeOut outfile
                                                                      in
-                                                                         reap (childpid,childin, childout); ()
+                                                                         reapWatcher (childpid,childin, childout); ()
                                                                      end)
                                                                  else
                                                                     ()
@@ -655,7 +774,7 @@
                                                                                val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
                                                                                val _ =  TextIO.closeOut outfile
                                                                            in
-                                                                              reap (childpid,childin, childout); ()
+                                                                              reapWatcher (childpid,childin, childout); ()
                                                                            end )
                                                                       else
                                                                          ()
@@ -674,7 +793,7 @@
                                                                                val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
                                                                                val _ =  TextIO.closeOut outfile
                                                                            in
-                                                                              reap (childpid,childin, childout); ()
+                                                                              reapWatcher (childpid,childin, childout); ()
                                                                            end )
                                                                       else
                                                                          ()

--- a/src/HOL/Tools/res_atp.ML	Sun May 22 19:26:18 2005 +0200
+++ b/src/HOL/Tools/res_atp.ML	Mon May 23 00:18:51 2005 +0200
@@ -185,14 +185,14 @@
                            (* without paramodulation *)
                            (warning ("goalstring in call_res_tac is: "^goalstring));
                            (warning ("prob file in cal_res_tac is: "^probfile));
-                                                       Watcher.callResProvers(childout,
-                            [("spass",thmstr,goalstring,spass_home,  
+                                                      (* Watcher.callResProvers(childout,
+                            [("spass",thmstr,goalstring,(*spass_home*),  
                              "-DocProof", 
-                             clasimpfile, axfile, hypsfile, probfile)]);
+                             clasimpfile, axfile, hypsfile, probfile)]);*)
 
                             Watcher.callResProvers(childout,
-                            [("spass",thmstr,goalstring,spass_home,  
-                             "-FullRed=0%-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", 
+                            [("spass",thmstr,goalstring(*,spass_home*),"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/spassshell",  
+                             "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", 
                              clasimpfile, axfile, hypsfile, probfile)]);
 
                            (* with paramodulation *)
@@ -302,6 +302,7 @@
         val _ = (warning ("clasimp_file is this: "^(File.sysify_path clasimp_file)) )  
 
         (* cq: add write out clasimps to file *)
+
         (* cq:create watcher and pass to isar_atp_aux *)
         (* tracing *) 
         (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
@@ -373,8 +374,8 @@
 (* what about clasimpset - it should already be in the ax file - perhaps append to ax file rather than just *)
 (* write out ? Or keep as a separate file and then cat them all together in the watcher, like we do with the *)
 (*claset file and prob file*)
-(* FIX*)
-fun isar_local_thms (delta_cs, delta_ss_thms) =
+(* FIX: update to work with clausify_axiom_pairs now in ResAxioms*)
+(*fun isar_local_thms (delta_cs, delta_ss_thms) =
     let val thms_cs = get_thms_cs delta_cs
 	val thms_ss = get_thms_ss delta_ss_thms
 	val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
@@ -384,7 +385,7 @@
     in
 	(ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out)
     end;
-
+*)
 
 
 
@@ -404,7 +405,7 @@
           (warning ("initial thm in isar_atp: "^thmstring));
           (warning ("subgoals in isar_atp: "^prems_string));
     	  (warning ("number of subgoals in isar_atp: "^(string_of_int prem_no)));
-          (isar_local_thms (d_cs,d_ss_thms); (warning("about to call isar_atp'"));
+          ((*isar_local_thms (d_cs,d_ss_thms); *)(warning("about to call isar_atp'"));
            isar_atp' (prems, thm))
     end;
 

--- a/src/HOL/Tools/res_axioms.ML	Sun May 22 19:26:18 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Mon May 23 00:18:51 2005 +0200
@@ -11,19 +11,18 @@
   val elimRule_tac : thm -> Tactical.tactic
   val elimR2Fol : thm -> term
   val transform_elim : thm -> thm
-  
-  val clausify_axiom : thm -> ResClause.clause list
+  val clausify_axiom_pairs : (string*thm) -> (ResClause.clause*thm) list
   val cnf_axiom : (string * thm) -> thm list
   val meta_cnf_axiom : thm -> thm list
   val cnf_rule : thm -> thm list
   val cnf_classical_rules_thy : theory -> thm list list * thm list
-  val clausify_classical_rules_thy : theory -> ResClause.clause list list * thm list
+ 
   val cnf_simpset_rules_thy : theory -> thm list list * thm list
-  val clausify_simpset_rules_thy : theory -> ResClause.clause list list * thm list
+ 
   val rm_Eps : (term * term) list -> thm list -> term list
   val claset_rules_of_thy : theory -> (string * thm) list
   val simpset_rules_of_thy : theory -> (string * thm) list
-  val clausify_rules : thm list -> thm list -> ResClause.clause list list * thm list
+  val clausify_rules_pairs : (string * thm) list -> thm list -> (ResClause.clause * thm) list list * thm list
   val setup : (theory -> theory) list
   end;
 
@@ -136,9 +135,13 @@
     let val tm = elimR2Fol th
 	val ctm = cterm_of (sign_of_thm th) tm	
     in
+
 	prove_goalw_cterm [] ctm (fn prems => [elimRule_tac th])
     end
-  else th;
+ else th;;	
+
+
+
 
 
 (**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
@@ -355,20 +358,6 @@
       in th' :: (rm_Eps epss' thms) end;
 
 
-(* convert a theorem into CNF and then into Clause.clause format. *)
-fun clausify_axiom th =
-    let val name = Thm.name_of_thm th
-	val isa_clauses = cnf_axiom (name, th)
-	      (*"isa_clauses" are already in "standard" form. *)
-        val isa_clauses' = rm_Eps [] isa_clauses
-        val clauses_n = length isa_clauses
-	fun make_axiom_clauses _ [] = []
-	  | make_axiom_clauses i (cls::clss) = 
-	      (ResClause.make_axiom_clause cls (name,i)) :: make_axiom_clauses (i+1) clss 
-    in
-	make_axiom_clauses 0 isa_clauses'		
-    end;
-  
 
 (**** Extract and Clausify theorems from a theory's claset and simpset ****)
 
@@ -408,21 +397,26 @@
 
 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****)
 
-(* classical rules *)
-fun clausify_rules [] err_list = ([],err_list)
-  | clausify_rules (th::thms) err_list =
-    let val (ts,es) = clausify_rules thms err_list
+(* outputs a list of (thm,clause) pairs *)
+fun clausify_axiom_pairs (thm_name,thm) =
+    let val isa_clauses = cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *)
+        val isa_clauses' = rm_Eps [] isa_clauses
+        val clauses_n = length isa_clauses
+	fun make_axiom_clauses _ [] []= []
+	  | make_axiom_clauses i (cls::clss) (cls'::clss')= ((ResClause.make_axiom_clause cls (thm_name,i)),cls') :: make_axiom_clauses (i+1) clss clss'
     in
-	((clausify_axiom th)::ts,es) handle  _ => (ts,(th::es))
+	make_axiom_clauses 0 isa_clauses' isa_clauses		
     end;
 
-(* convert all classical rules from a given theory into Clause.clause format. *)
-fun clausify_classical_rules_thy thy =
-    clausify_rules (map #2 (claset_rules_of_thy thy)) [];
 
-(* convert all simplifier rules from a given theory into Clause.clause format. *)
-fun clausify_simpset_rules_thy thy =
-    clausify_rules (map #2 (simpset_rules_of_thy thy)) [];
+fun clausify_rules_pairs [] err_list = ([],err_list)
+  | clausify_rules_pairs ((name,thm)::thms) err_list =
+    let val (ts,es) = clausify_rules_pairs thms err_list
+    in
+	((clausify_axiom_pairs (name,thm))::ts,es) handle  _ => (ts,(thm::es))
+    end;
+(* classical rules *)
+
 
 (*Setup function: takes a theory and installs ALL simprules and claset rules 
   into the clause cache*)

--- a/src/HOL/Tools/res_clause.ML	Sun May 22 19:26:18 2005 +0200
+++ b/src/HOL/Tools/res_clause.ML	Mon May 23 00:18:51 2005 +0200
@@ -30,6 +30,7 @@
     val tptp_arity_clause : arityClause -> string
     val tptp_classrelClause : classrelClause -> string
     val tptp_clause : clause -> string list
+    val clause_info : clause ->  string * string
     val tptp_clauses2str : string list -> string
     val typed : unit -> unit
     val untyped : unit -> unit
@@ -643,6 +644,14 @@
 	cls_str :: (typ_clss 0 tfree_lits)
     end;
 
+fun clause_info cls =
+    let 
+	val cls_id = string_of_clauseID cls
+	val ax_name = string_of_axiomName cls
+    in 
+	((ax_name^""), cls_id)
+    end;
+
 
 fun clause2tptp cls =
     let val (lits,tfree_lits) = tptp_clause_aux cls (*"lits" includes the typing assumptions (TVars)*)