Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
authorquigley
Tue May 31 12:42:36 2005 +0200 (2005-05-31)
changeset 161562f6fc19aba1e
parent 16155 a6403c6c5339
child 16157 1764cc98bafd
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
ruleset.
src/HOL/Tools/ATP/SpassCommunication.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
     1.1 --- a/src/HOL/Tools/ATP/SpassCommunication.ML	Tue May 31 12:36:01 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/SpassCommunication.ML	Tue May 31 12:42:36 2005 +0200
     1.3 @@ -7,6 +7,20 @@
     1.4  (***************************************************************************)
     1.5  (*  Code to deal with the transfer of proofs from a Spass process          *)
     1.6  (***************************************************************************)
     1.7 +signature SPASS_COMM =
     1.8 +  sig
     1.9 +    val reconstruct : bool ref
    1.10 +    val getSpassInput : TextIO.instream -> string * string * string
    1.11 +    val checkSpassProofFound:  TextIO.instream * TextIO.outstream * Posix.Process.pid * string * 
    1.12 +                               string *string * Thm.thm * int *(ResClause.clause * Thm.thm) Array.array  * int -> bool
    1.13 +    
    1.14 +  end;
    1.15 +
    1.16 +structure SpassComm :SPASS_COMM =
    1.17 +struct
    1.18 +
    1.19 +(* switch for whether to reconstruct a proof found, or just list the lemmas used *)
    1.20 +val reconstruct = ref true;
    1.21  
    1.22  (***********************************)
    1.23  (*  Write Spass   output to a file *)
    1.24 @@ -42,7 +56,13 @@
    1.25   in
    1.26  SELECT_GOAL
    1.27    (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 
    1.28 -  METAHYPS(fn negs => (Recon_Transfer.spassString_to_reconString proofextract thmstring goalstring toParent ppid negs clause_arr  num_of_clauses ))]) sg_num
    1.29 +  METAHYPS(fn negs => (if !reconstruct 
    1.30 +		       then 
    1.31 +			   Recon_Transfer.spassString_to_reconString proofextract thmstring goalstring 
    1.32 +								     toParent ppid negs clause_arr  num_of_clauses 
    1.33 +		       else
    1.34 +			   Recon_Transfer.spassString_to_lemmaString proofextract thmstring goalstring 
    1.35 +								     toParent ppid negs clause_arr  num_of_clauses ))]) sg_num	
    1.36   end ;
    1.37  
    1.38  
    1.39 @@ -111,7 +131,7 @@
    1.40  fun checkSpassProofFound (fromChild, toParent, ppid,thmstring,goalstring, childCmd, thm, sg_num, clause_arr,  (num_of_clauses:int )) = 
    1.41                                         let val spass_proof_file =  TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "spass_proof")))
    1.42                                              val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_checkspass")));                                                                            
    1.43 -                                            val _ = TextIO.output (outfile, "checking proof found, thm is: "^(string_of_thm thm))
    1.44 +                                            val _ = TextIO.output (outfile, "checking if proof found, thm is: "^(string_of_thm thm))
    1.45                                               
    1.46                                              val _ =  TextIO.closeOut outfile
    1.47                                         in 
    1.48 @@ -140,8 +160,8 @@
    1.49                                                               val _ =  TextIO.closeOut outfile
    1.50                                                        in
    1.51                                                         
    1.52 -                                                        (*TextIO.output (toParent,childCmd^"\n" );
    1.53 -                                                        TextIO.flushOut toParent;*)
    1.54 +                                                        TextIO.output (toParent,childCmd^"\n" );
    1.55 +                                                        TextIO.flushOut toParent;
    1.56                                                          TextIO.output (spass_proof_file, (thisLine));
    1.57                                                          TextIO.flushOut spass_proof_file;
    1.58                                                          TextIO.closeOut spass_proof_file;
    1.59 @@ -224,6 +244,18 @@
    1.60                                                   (reconstr, thmstring, goalstring)
    1.61                                               end
    1.62                                            )
    1.63 +
    1.64 +					else if (String.isPrefix   "Rules from"  thisLine)
    1.65 +                                        then 
    1.66 +                                          (
    1.67 +                                             let val reconstr = thisLine
    1.68 +                                                 val thmstring = TextIO.inputLine instr
    1.69 +                                                 val goalstring = TextIO.inputLine instr
    1.70 +                                             in
    1.71 +                                                 (reconstr, thmstring, goalstring)
    1.72 +                                             end
    1.73 +                                          )
    1.74 +
    1.75                                           else if (thisLine = "Proof found but translation failed!")
    1.76                                                then
    1.77    						(
    1.78 @@ -245,3 +277,4 @@
    1.79                                ("No output from reconstruction process.\n","","")
    1.80  
    1.81  
    1.82 +end;
     2.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue May 31 12:36:01 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue May 31 12:42:36 2005 +0200
     2.3 @@ -1,6 +1,7 @@
     2.4 +
     2.5  (*  ID:         $Id$
     2.6 -    Author:     Claire Quigley
     2.7 -    Copyright   2004  University of Cambridge
     2.8 + Author:     Claire Quigley
     2.9 + Copyright   2004  University of Cambridge
    2.10  *)
    2.11  
    2.12  (******************)
    2.13 @@ -195,19 +196,66 @@
    2.14  |   retrieve_axioms clause_arr  (x::xs) =  [Array.sub(clause_arr, x)]@
    2.15   						     (retrieve_axioms clause_arr  xs)
    2.16  
    2.17 +fun subone x = x - 1
    2.18 +
    2.19 +fun numstr [] = ""
    2.20 +|   numstr (x::xs) = (string_of_int x)^"%"^(numstr xs)
    2.21 +
    2.22  
    2.23  (* retrieve the axioms that were obtained from the clasimpset *)
    2.24  
    2.25  fun get_clasimp_cls clause_arr clasimp_num step_nums = 
    2.26 -                                let val clasimp_nums = List.filter (is_clasimp_ax clasimp_num) step_nums
    2.27 +                                let 
    2.28 +                                    val realnums = map subone step_nums
    2.29 +                                   
    2.30 + 				    
    2.31 +                                    val clasimp_nums = List.filter (is_clasimp_ax (clasimp_num - 1)) realnums
    2.32 +                                   val axnums = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "axnums")))     
    2.33 +                                   val _ = TextIO.output(axnums,(numstr clasimp_nums))
    2.34 +                                   val _ = TextIO.closeOut(axnums)
    2.35                                  in
    2.36                                      retrieve_axioms clause_arr  clasimp_nums
    2.37                                  end
    2.38  
    2.39 +fun get_cls []  = []
    2.40 +|   get_cls (x::xs) = ((#1 x)::(get_cls xs))
    2.41 +
    2.42 +(* add array and table here, so can retrieve clasimp axioms *)
    2.43 +
    2.44 + fun get_axiom_names proof_steps thms (clause_arr:(ResClause.clause * Thm.thm) Array.array) num_of_clauses  =
    2.45 +                                         let 
    2.46 +                                           (* not sure why this is necessary again, but seems to be *)
    2.47 +					    val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    2.48 +                                            val axioms = get_init_axioms proof_steps
    2.49 +                                            val step_nums = get_step_nums axioms []
    2.50 +
    2.51 +                                           (***********************************************)
    2.52 +                                           (* here need to add the clauses from clause_arr*)
    2.53 +                                           (***********************************************)
    2.54 +
    2.55 +                                            val (clasimp_names_cls) = get_clasimp_cls clause_arr   num_of_clauses step_nums 
    2.56 +                                            val clauses=(get_cls clasimp_names_cls) 
    2.57 +                                            val (names_clsnums) = map ResClause.clause_info clauses
    2.58 +                                            val clasimp_names = map fst names_clsnums
    2.59 +
    2.60 +                                            val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "clasimp_names")))                                                                   val clasimp_namestr = concat clasimp_names                            
    2.61 +                                            val _ = TextIO.output (outfile,clasimp_namestr)
    2.62 +                                            val _ =  TextIO.closeOut outfile
    2.63 +					    val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
    2.64 +                                           
    2.65 +                                         in
    2.66 +                                            (clasimp_names)
    2.67 +                                         end
    2.68 +    
    2.69 +fun numclstr (vars, []) str = str
    2.70 +|   numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
    2.71 +in
    2.72 +numclstr  (vars,rest) newstr
    2.73 +end
    2.74  
    2.75  
    2.76 +fun addvars  c (a,b)  = (a,b,c)
    2.77  
    2.78 -(* add array and table here, so can retrieve clasimp axioms *)
    2.79  
    2.80   fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
    2.81       let 
    2.82 @@ -293,32 +341,8 @@
    2.83  	(distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas)))
    2.84       end
    2.85      
    2.86 -fun numclstr (vars, []) str = str
    2.87 -|   numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
    2.88 -in
    2.89 -numclstr  (vars,rest) newstr
    2.90 -end
    2.91  
    2.92 -(*
    2.93 -
    2.94 -val proofstr = "Did parsing on Here is a proof with depth 4, length 9 :\
    2.95 -\1[0:Inp] || v_P(tconst_fun(typ__da_a,tconst_bool),v_x)*+ -> v_P(tconst_fun(typ__da_a,tconst_bool),U)*.\
    2.96 -\3[0:Inp] || v_P(tconst_fun(typ__da_a,tconst_bool),U)*+ -> v_P(tconst_fun(typ__da_a,tconst_bool),v_x)*.\
    2.97 -\5[0:Inp] ||  -> v_P(tconst_fun(typ__da_a,tconst_bool),U)* v_P(tconst_fun(typ__da_a,tconst_bool),v_xa)*.\
    2.98 -\7[0:Inp] || v_P(tconst_fun(typ__da_a,tconst_bool),U)*+ v_P(tconst_fun(typ__da_a,tconst_bool),v_xb)* -> .\
    2.99 -\9[0:Fac:5.0,5.1] ||  -> v_P(tconst_fun(typ__da_a,tconst_bool),v_xa)*.\
   2.100 -\10[0:Res:9.0,3.0] ||  -> v_P(tconst_fun(typ__da_a,tconst_bool),v_x)*.\
   2.101 -\11[0:Res:10.0,1.0] ||  -> v_P(tconst_fun(typ__da_a,tconst_bool),U)*.\
   2.102 -\12[0:Fac:7.0,7.1] || v_P(tconst_fun(typ__da_a,tconst_bool),v_xb)* -> .\
   2.103 -\14[0:Res:11.0,12.0] ||  -> .\
   2.104 -\Formulae used in the proof :"
   2.105 -
   2.106 -*)
   2.107 -
   2.108 -
   2.109 -fun addvars  c (a,b)  = (a,b,c)
   2.110 -
   2.111 -
   2.112 +                                        
   2.113  
   2.114  (*********************************************************************)
   2.115  (* Pass in spass string of proof and string version of isabelle goal *)
   2.116 @@ -326,52 +350,74 @@
   2.117  (*********************************************************************)
   2.118  
   2.119  
   2.120 -(*
   2.121 -
   2.122 +fun rules_to_string [] str = str
   2.123 +|   rules_to_string [x] str = str^x
   2.124 +|   rules_to_string (x::xs) str = rules_to_string xs (str^x^"   ")
   2.125 +                                  
   2.126  
   2.127 -val proofstr = "Here is a proof with depth 2, length 5 :\
   2.128 -\1[0:Inp] ||  -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\
   2.129 -\3[0:Inp] || v_Q(tconst_fun(typ__asc39_a,tconst_bool),U)* -> .\
   2.130 -\5[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)* -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa).\
   2.131 -\7[0:Res:1.0,5.0] ||  -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa)*.\
   2.132 -\9[0:Res:7.0,3.0] ||  -> .\
   2.133 -\Formulae used in the proof :"
   2.134 +val dummy_tac = PRIMITIVE(fn thm => thm );
   2.135  
   2.136  
   2.137 -val proofstr = "Here is a proof with depth 4, length 9 :\
   2.138 -\1[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)*+ -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\
   2.139 -\3[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*+ -> v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)*.\
   2.140 -\5[0:Inp] ||  -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)* v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xa)*.\
   2.141 -\7[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*+ v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xb)* -> .\
   2.142 -\9[0:Fac:5.0,5.1] ||  -> v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xa)*.\
   2.143 -\10[0:Res:9.0,3.0] ||  -> v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x)*.\
   2.144 -\11[0:Res:10.0,1.0] ||  -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\
   2.145 -\12[0:Fac:7.0,7.1] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_xb)* -> .\
   2.146 -\14[0:Res:11.0,12.0] ||  -> .\
   2.147 -\Formulae used in the proof :";
   2.148 +fun spassString_to_lemmaString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   2.149 +           let val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));     						  val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr^"goalstr is: "^goalstring^" num of clauses is: "^(string_of_int num_of_clauses)))
   2.150 +                                                  val _ =  TextIO.closeOut outfile
   2.151 +
   2.152 +                                              (***********************************)
   2.153 +                                              (* parse spass proof into datatype *)
   2.154 +                                              (***********************************)
   2.155 +         
   2.156 +                                                  val tokens = #1(lex proofstr)
   2.157 +                                                  val proof_steps1 = parse tokens
   2.158 +                                                  val proof_steps = just_change_space proof_steps1
   2.159 +                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse")));                                                     val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   2.160 +                                                  val _ =  TextIO.closeOut outfile
   2.161 +                                                
   2.162 +                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thmstring_at_parse")));                                        val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
   2.163 +                                                  val _ =  TextIO.closeOut outfile
   2.164 +                                              (************************************)
   2.165 +                                              (* recreate original subgoal as thm *)
   2.166 +                                              (************************************)
   2.167 +                                                
   2.168 +                                                  (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   2.169 +                                                  (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
   2.170 +                                                  (* subgoal this is, and turn it into meta_clauses *)
   2.171 +                                                  (* should prob add array and table here, so that we can get axioms*)
   2.172 +                                                  (* produced from the clasimpset rather than the problem *)
   2.173 +
   2.174 +                                                  val (axiom_names) = get_axiom_names proof_steps  thms clause_arr  num_of_clauses
   2.175 +                                                  val ax_str = "Rules from clasimpset used in proof found by SPASS: "^(rules_to_string axiom_names "")
   2.176 +                                                  val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "reconstrfile")));                                                     val _ = TextIO.output (outfile, ("reconstring is: "^ax_str^"  "^goalstring))
   2.177 +                                                  val _ =  TextIO.closeOut outfile
   2.178 +                                                   
   2.179 +                                              in 
   2.180 +                                                   TextIO.output (toParent, ax_str^"\n");
   2.181 +                                                   TextIO.flushOut toParent;
   2.182 +                                        	   TextIO.output (toParent, "goalstring: "^goalstring^"\n");
   2.183 +                                         	   TextIO.flushOut toParent;
   2.184 +                                         	   TextIO.output (toParent, "thmstring: "^thmstring^"\n");
   2.185 +                                         	   TextIO.flushOut toParent;
   2.186 +                                          
   2.187 +                                         	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   2.188 +                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
   2.189 +                                         	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   2.190 +                                              end
   2.191 +                                              handle _ => (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
   2.192 +
   2.193 +                                                  val _ = TextIO.output (outfile, ("In exception handler"));
   2.194 +                                                  val _ =  TextIO.closeOut outfile
   2.195 +                                              in 
   2.196 +                                                  TextIO.output (toParent,"Proof found but translation failed!" ^"\n");
   2.197 +                                                  TextIO.flushOut toParent;
   2.198 +						   TextIO.output (toParent, thmstring^"\n");
   2.199 +                                         	   TextIO.flushOut toParent;
   2.200 +                                         	   TextIO.output (toParent, goalstring^"\n");
   2.201 +                                         	   TextIO.flushOut toParent;
   2.202 +            					  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   2.203 +                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
   2.204 +                                         	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   2.205 +                                              end)
   2.206  
   2.207  
   2.208 -val thmstring = " (~ (P::'a::type => bool) (x::'a::type) | P (U::'a::type)) & (~ (P::'a::type => bool) (U::'a::type) | P (x::'a::type)) & ((P::'a::type => bool) (xa::'a::type) | P (U::'a::type)) & (~ (P::'a::type => bool) (U::'a::type) | ~ P (xb::'a::type))";
   2.209 -
   2.210 -val thmstring = "(ALL xb::'a::type.   (~ (P::'a::type => bool) ((x::'a::type => 'a::type) xb) |    (Q::'a::type => bool) ((xa::'a::type => 'a::type) xb)) &   P xb & ~ Q xb)"
   2.211 -
   2.212 -
   2.213 -val thmstring ="(ALL xb::'a::type.   (~ (P::'a::type => bool) ((x::'a::type => 'a::type) xb) |    (Q::'a::type => bool) ((xa::'a::type => 'a::type) xb)) &   P xb & ~ Q xb)"
   2.214 -
   2.215 -val proofstr = "Did parsing on Here is a proof with depth 2, length 5 :\
   2.216 -\1[0:Inp] ||  -> v_P(tconst_fun(typ__asc39_a,tconst_bool),U)*.\
   2.217 -\3[0:Inp] || v_Q(tconst_fun(typ__asc39_a,tconst_bool),U)* -> .\
   2.218 -\5[0:Inp] || v_P(tconst_fun(typ__asc39_a,tconst_bool),v_x(tconst_fun(typ__asc39_a,typ__asc39_a),U))* -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa(tconst_fun(typ__asc39_a,typ__asc39_a),U)).\
   2.219 -\7[0:Res:1.0,5.0] ||  -> v_Q(tconst_fun(typ__asc39_a,tconst_bool),v_xa(tconst_fun(typ__asc39_a,typ__asc39_a),U))*.\
   2.220 -\9[0:Res:7.0,3.0] ||  -> .\
   2.221 -\Formulae used in the proof :";
   2.222 -
   2.223 -*)
   2.224 -
   2.225 -
   2.226 -
   2.227 -
   2.228 -val dummy_tac = PRIMITIVE(fn thm => thm );
   2.229  
   2.230  fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   2.231        let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));                                        
   2.232 @@ -474,10 +520,6 @@
   2.233  
   2.234  
   2.235  
   2.236 -
   2.237 -
   2.238 -
   2.239 -
   2.240  (**********************************************************************************)
   2.241  (* At other end, want to turn back into datatype so can apply reconstruct_proof.  *)
   2.242  (* This will be done by the signal handler                                        *)
   2.243 @@ -808,4 +850,6 @@
   2.244                                 end 
   2.245  
   2.246  
   2.247 +
   2.248 +
   2.249  end;
     3.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Tue May 31 12:36:01 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Tue May 31 12:42:36 2005 +0200
     3.3 @@ -5,7 +5,7 @@
     3.4      Copyright   2004  University of Cambridge
     3.5  *)
     3.6  
     3.7 -signature RES_CLASIMP =
     3.8 +signature RES_CLASIMP = 
     3.9    sig
    3.10       val write_out_clasimp :string -> (ResClause.clause * Thm.thm) Array.array * int
    3.11    end;
    3.12 @@ -50,6 +50,30 @@
    3.13  (*Insert th into the result provided the name is not "".*)
    3.14  fun add_nonempty ((name,th), ths) = if name="" then ths else th::ths;
    3.15  
    3.16 +fun posinlist x [] n = "not in list"
    3.17 +|   posinlist x (y::ys) n = if (x=y) 
    3.18 +			    then
    3.19 + 				string_of_int n
    3.20 +			    else posinlist x (ys) (n+1)
    3.21 +
    3.22 +
    3.23 +fun pairup [] [] = []
    3.24 +|   pairup (x::xs) (y::ys) = (x,y)::(pairup xs ys)
    3.25 +
    3.26 +fun multi x 0 xlist = xlist
    3.27 +   |multi x n xlist = multi x (n -1 ) (x::xlist);
    3.28 +
    3.29 +
    3.30 +fun clause_numbering ((clause, theorem), cls) = let val num_of_cls = length cls
    3.31 +                                              val numbers = 0 upto (num_of_cls -1)
    3.32 +                                              val multi_name = multi (clause, theorem)  num_of_cls []
    3.33 +                                          in 
    3.34 +                                              (multi_name)
    3.35 +                                          end;
    3.36 +
    3.37 +
    3.38 +
    3.39 + 
    3.40  
    3.41  fun write_out_clasimp filename = 
    3.42      let val claset_rules = ResAxioms.claset_rules_of_thy (the_context());
    3.43 @@ -64,22 +88,25 @@
    3.44  
    3.45  	val cls_thms = (claset_cls_thms@simpset_cls_thms);
    3.46  	val cls_thms_list = List.concat cls_thms;
    3.47 -
    3.48 -	(*********************************************************)
    3.49 -	(* create array and put clausename, number pairs into it *)
    3.50 -	(*********************************************************)
    3.51 -	val num_of_clauses =  0;
    3.52 -	val clause_arr = Array.fromList cls_thms_list;
    3.53 -
    3.54 -	val num_of_clauses = List.length cls_thms_list;
    3.55 -
    3.56 +        (* length 1429 *)
    3.57  	(*************************************************)
    3.58  	(* Write out clauses as tptp strings to filename *)
    3.59  	(*************************************************)
    3.60  	val clauses = map #1(cls_thms_list);
    3.61  	val cls_tptp_strs = map ResClause.tptp_clause clauses;
    3.62 +        val alllist = pairup cls_thms_list cls_tptp_strs
    3.63 +        val whole_list = List.concat (map clause_numbering alllist);
    3.64 + 
    3.65 +        (*********************************************************)
    3.66 +	(* create array and put clausename, number pairs into it *)
    3.67 +	(*********************************************************)
    3.68 +	val num_of_clauses =  0;
    3.69 +	val clause_arr = Array.fromList whole_list;
    3.70 +	val num_of_clauses = List.length whole_list;
    3.71 +
    3.72  	(* list of lists of tptp string clauses *)
    3.73  	val stick_clasrls =   List.concat cls_tptp_strs;
    3.74 +        (* length 1581*)
    3.75  	val out = TextIO.openOut filename;
    3.76  	val _=   ResLib.writeln_strs out stick_clasrls;
    3.77  	val _= TextIO.flushOut out;
    3.78 @@ -88,6 +115,7 @@
    3.79  	(clause_arr, num_of_clauses)
    3.80    end;
    3.81  
    3.82 -
    3.83  end;
    3.84  
    3.85 +
    3.86 +	
     4.1 --- a/src/HOL/Tools/ATP/watcher.ML	Tue May 31 12:36:01 2005 +0200
     4.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Tue May 31 12:42:36 2005 +0200
     4.3 @@ -1,4 +1,5 @@
     4.4  (*  Title:      Watcher.ML
     4.5 +
     4.6      ID:         $Id$
     4.7      Author:     Claire Quigley
     4.8      Copyright   2004  University of Cambridge
     4.9 @@ -162,27 +163,28 @@
    4.10  	  val _ = File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))                                                                     
    4.11  	              (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n")
    4.12  	 (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
    4.13 -	  val probID = ReconOrderClauses.last(explode probfile)
    4.14 +	 val probID = ReconOrderClauses.last(explode probfile)
    4.15  	  val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
    4.16  	  (*** only include problem and clasimp for the moment, not sure how to refer to ***)
    4.17 -	  (*** hyps/local axioms just now                                                ***)
    4.18 -          (*FIXME: find a way that works for SML/NJ too: it regards > as a filename!*)
    4.19 -	  val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile,  ">", (File.sysify_path wholefile)])
    4.20 +
    4.21 +	  (*** hyps/local axioms just now (*,axfile, hypsfile,*)                                               ***)
    4.22 +	  val whole_prob_file = system ("/bin/cat " ^ clasimpfile ^" "^ probfile ^ " > " ^ (File.sysify_path wholefile))
    4.23 +
    4.24  	  val dfg_create = if File.exists dfg_dir 
    4.25  			   then warning("dfg dir exists")
    4.26  			   else File.mkdir dfg_dir; 
    4.27  	  
    4.28  	  val dfg_path = File.sysify_path dfg_dir;
    4.29 -	  val tptp2x_args = ["-fdfg", "-d " ^ dfg_path, File.sysify_path wholefile]
    4.30  	  val exec_tptp2x = 
    4.31 - 	      Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X", tptp2x_args)
    4.32 +	        Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X",  
    4.33 +	                     ["-fdfg", "-d " ^ dfg_path, File.sysify_path wholefile])
    4.34  	(*val _ = Posix.Process.wait ()*)
    4.35  	(*val _ =Unix.reap exec_tptp2x*)
    4.36  	  val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
    4.37   
    4.38         in   
    4.39  	  goals_being_watched := (!goals_being_watched) + 1;
    4.40 -	  Posix.Process.sleep(Time.fromSeconds 4); 
    4.41 +	  Posix.Process.sleep(Time.fromSeconds 1); 
    4.42  	  (warning ("probfile is: "^probfile));
    4.43  	  (warning("dfg file is: "^newfile));
    4.44  	  (warning ("wholefile is: "^(File.sysify_path wholefile)));
    4.45 @@ -195,8 +197,8 @@
    4.46  	  if File.exists
    4.47  	        (Path.append dfg_dir (Path.basic ("ax_prob"^"_" ^ probID ^ ".dfg")))
    4.48  	  then callResProvers (toWatcherStr, args)
    4.49 -	  else error ("tptp2X failed: " ^ getenv "TPTP2X_HOME" ^ "/tptp2X " ^
    4.50 -	              space_implode " " tptp2x_args)
    4.51 +	  else error ("tptp2X failed: " ^ getenv "TPTP2X_HOME" ^ "/tptp2X" ^
    4.52 +	              " -fdfg " ^ File.sysify_path wholefile ^ " -d " ^ dfg_path)
    4.53        end
    4.54  (*
    4.55  fun callResProversStr (toWatcherStr,  []) =  "End of calls\n" 
    4.56 @@ -381,7 +383,7 @@
    4.57  			 in 
    4.58  			 if (isSome pd ) then 
    4.59  			     let val pd' = OS.IO.pollIn (valOf pd)
    4.60 -				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
    4.61 +				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
    4.62  			     in
    4.63  				if null pdl 
    4.64  				then
    4.65 @@ -407,7 +409,7 @@
    4.66  			 in 
    4.67  			 if (isSome pd ) then 
    4.68  			     let val pd' = OS.IO.pollIn (valOf pd)
    4.69 -				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
    4.70 +				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 2000)) 
    4.71  			     in
    4.72  				if null pdl 
    4.73  				then
    4.74 @@ -456,7 +458,7 @@
    4.75  			  (* check here for prover label on child*)
    4.76  			  let val _ = File.write (File.tmp_path (Path.basic "child_incoming"))  ("subgoals forked to checkChildren: "^prems_string^prover^thmstring^goalstring^childCmd) 
    4.77  		      val childDone = (case prover of
    4.78 -	    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
    4.79 +	    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (SpassComm.checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
    4.80  			   in
    4.81  			    if childDone      (**********************************************)
    4.82  			    then              (* child has found a proof and transferred it *)
    4.83 @@ -700,81 +702,123 @@
    4.84  		status
    4.85  	end
    4.86  
    4.87 -fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = 
    4.88 -  let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
    4.89 -      val streams =snd mychild
    4.90 -      val childin = fst streams
    4.91 -      val childout = snd streams
    4.92 -      val childpid = fst mychild
    4.93 -      val sign = sign_of_thm thm
    4.94 -      val prems = prems_of thm
    4.95 -      val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
    4.96 -      val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
    4.97 -      fun vampire_proofHandler (n) =
    4.98 -	    (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
    4.99 -	    getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )               
   4.100 -     
   4.101 +
   4.102 +fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
   4.103 +			   val streams =snd mychild
   4.104 +                           val childin = fst streams
   4.105 +                           val childout = snd streams
   4.106 +                           val childpid = fst mychild
   4.107 +                           val sign = sign_of_thm thm
   4.108 +                           val prems = prems_of thm
   4.109 +                           val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   4.110 +                           val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
   4.111 +                           fun vampire_proofHandler (n) =
   4.112 +                           (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   4.113 +                           getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )               
   4.114 +                          
   4.115 +
   4.116 +fun spass_proofHandler (n) = (
   4.117 +                                 let  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
   4.118 +                                      val _ = TextIO.output (outfile, ("In signal handler now\n"))
   4.119 +                                      val _ =  TextIO.closeOut outfile
   4.120 +                                      val (reconstr, thmstring, goalstring) = SpassComm.getSpassInput childin
   4.121 +                                      val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
   4.122 +
   4.123 +                                      val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
   4.124 +                                      val _ =  TextIO.closeOut outfile
   4.125 +                                      in          (* if a proof has been found and sent back as a reconstruction proof *)
   4.126 +                                                  if ( (substring (reconstr, 0,1))= "[")
   4.127 +                                                  then 
   4.128  
   4.129 -      fun spass_proofHandler (n) = (
   4.130 -	let val _ = File.write (File.tmp_path (Path.basic "foo_signal1")) "In signal handler now\n"
   4.131 -	    val (reconstr, thmstring, goalstring) = getSpassInput childin
   4.132 -	    val _ = File.append (File.tmp_path (Path.basic "foo_signal"))
   4.133 -	              ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched)))
   4.134 -        in (* if a proof has been found and sent back as a reconstruction proof *)
   4.135 -	  if ( (substring (reconstr, 0,1))= "[")
   4.136 -	  then 
   4.137 -	    (
   4.138 -	     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   4.139 -	     Recon_Transfer.apply_res_thm reconstr goalstring;
   4.140 -	     Pretty.writeln(Pretty.str  (oct_char "361"));
   4.141 -	     
   4.142 -	     goals_being_watched := ((!goals_being_watched) - 1);
   4.143 -     
   4.144 -	     if ((!goals_being_watched) = 0)
   4.145 -	     then 
   4.146 -		(let val _ = File.write (File.tmp_path (Path.basic "foo_reap_found"))
   4.147 -		     ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")
   4.148 -		 in
   4.149 -		     reapWatcher (childpid,childin, childout); ()
   4.150 -		 end)
   4.151 -	     else ()
   4.152 -	    )
   4.153 -	    (* if there's no proof, but a message from Spass *)
   4.154 -	    else if ((substring (reconstr, 0,5))= "SPASS")
   4.155 -		 then
   4.156 -		    (goals_being_watched := (!goals_being_watched) -1;
   4.157 -		     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   4.158 -		      Pretty.writeln(Pretty.str (goalstring^reconstr));
   4.159 -		      Pretty.writeln(Pretty.str  (oct_char "361"));
   4.160 -		      if (!goals_being_watched = 0)
   4.161 -		      then 
   4.162 -			  (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   4.163 -			       ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
   4.164 -			   reapWatcher (childpid,childin, childout); ())
   4.165 -		      else
   4.166 -			 ()
   4.167 -		)
   4.168 -		  (* if proof translation failed *)
   4.169 -		  else if ((substring (reconstr, 0,5)) = "Proof")
   4.170 -		  then 
   4.171 -		     (goals_being_watched := (!goals_being_watched) -1;
   4.172 -		      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   4.173 -		       Pretty.writeln(Pretty.str (goalstring^reconstr));
   4.174 -		       Pretty.writeln(Pretty.str  (oct_char "361"));
   4.175 -		       if (!goals_being_watched = 0)
   4.176 -		       then 
   4.177 -			  (File.write(File.tmp_path (Path.basic "foo_reap_comp"))
   4.178 -			      ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
   4.179 -			   reapWatcher (childpid,childin, childout); ())		       
   4.180 -		       else ())
   4.181 -	 	  else () (* add something here ?*)
   4.182 -	     end)
   4.183 +                                                            (
   4.184 +                                                                 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   4.185 +                                                                 Recon_Transfer.apply_res_thm reconstr goalstring;
   4.186 +                                                                 Pretty.writeln(Pretty.str  (oct_char "361"));
   4.187 +                                                                 
   4.188 +                                                                 goals_being_watched := ((!goals_being_watched) - 1);
   4.189 +                                                         
   4.190 +                                                                 if ((!goals_being_watched) = 0)
   4.191 +                                                                 then 
   4.192 +                                                                    (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_found")));
   4.193 +                                                                         val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   4.194 +                                                                         val _ =  TextIO.closeOut outfile
   4.195 +                                                                     in
   4.196 +                                                                         killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   4.197 +                                                                     end)
   4.198 +                                                                 else
   4.199 +                                                                    ()
   4.200 +                                                            )
   4.201 +                                                    (* if there's no proof, but a message from Spass *)
   4.202 +                                                    else if ((substring (reconstr, 0,5))= "SPASS")
   4.203 +                                                         then
   4.204 +                                                                 (
   4.205 +                                                                     goals_being_watched := (!goals_being_watched) -1;
   4.206 +                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   4.207 +                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
   4.208 +                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
   4.209 +                                                                      if (!goals_being_watched = 0)
   4.210 +                                                                      then 
   4.211 +                                                                          (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
   4.212 +                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   4.213 +                                                                               val _ =  TextIO.closeOut outfile
   4.214 +                                                                           in
   4.215 +                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   4.216 +                                                                           end )
   4.217 +                                                                      else
   4.218 +                                                                         ()
   4.219 +                                                                ) 
   4.220 +						   (* print out a list of rules used from clasimpset*)
   4.221 +                                                    else if ((substring (reconstr, 0,5))= "Rules")
   4.222 +                                                         then
   4.223 +                                                                 (
   4.224 +                                                                     goals_being_watched := (!goals_being_watched) -1;
   4.225 +                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   4.226 +                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
   4.227 +                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
   4.228 +                                                                      if (!goals_being_watched = 0)
   4.229 +                                                                      then 
   4.230 +                                                                          (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
   4.231 +                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   4.232 +                                                                               val _ =  TextIO.closeOut outfile
   4.233 +                                                                           in
   4.234 +                                                                              killWatcher (childpid);  reapWatcher (childpid,childin, childout);()
   4.235 +                                                                           end )
   4.236 +                                                                      else
   4.237 +                                                                         ()
   4.238 +                                                                )
   4.239 +							
   4.240 +                                                          (* if proof translation failed *)
   4.241 +                                                          else if ((substring (reconstr, 0,5)) = "Proof")
   4.242 +                                                               then 
   4.243 +                                                                   (
   4.244 +                                                                     goals_being_watched := (!goals_being_watched) -1;
   4.245 +                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   4.246 +                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
   4.247 +                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
   4.248 +                                                                      if (!goals_being_watched = 0)
   4.249 +                                                                      then 
   4.250 +                                                                          (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
   4.251 +                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   4.252 +                                                                               val _ =  TextIO.closeOut outfile
   4.253 +                                                                           in
   4.254 +                                                                              killWatcher (childpid); reapWatcher (childpid,childin, childout); ()
   4.255 +                                                                           end )
   4.256 +                                                                      else
   4.257 +                                                                         ()
   4.258 +                                                                )
   4.259  
   4.260  
   4.261 -   
   4.262 -  in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
   4.263 -     IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
   4.264 -     (childin, childout, childpid)
   4.265 +                                                                else  (* add something here ?*)
   4.266 +                                                                   ()
   4.267 +                                                             
   4.268 +                                       end)
   4.269 +
   4.270 +
   4.271 +                        
   4.272 +                       in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
   4.273 +                          IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
   4.274 +                          (childin, childout, childpid)
   4.275 +
   4.276  
   4.277    end
   4.278  
     5.1 --- a/src/HOL/Tools/res_atp.ML	Tue May 31 12:36:01 2005 +0200
     5.2 +++ b/src/HOL/Tools/res_atp.ML	Tue May 31 12:42:36 2005 +0200
     5.3 @@ -21,7 +21,7 @@
     5.4  (*val atp_ax_tac : Thm.thm list -> int -> Tactical.tactic*)
     5.5  (*val atp_tac : int -> Tactical.tactic*)
     5.6  val debug: bool ref
     5.7 -
     5.8 +val full_spass: bool ref
     5.9  end;
    5.10  
    5.11  structure ResAtp : RES_ATP =
    5.12 @@ -38,6 +38,7 @@
    5.13  (* default value is false *)
    5.14  
    5.15  val trace_res = ref false;
    5.16 +val full_spass = ref false;
    5.17  
    5.18  val skolem_tac = skolemize_tac;
    5.19  
    5.20 @@ -188,11 +189,19 @@
    5.21       [("spass",thmstr,goalstring,*spass_home*,  
    5.22       "-DocProof", 
    5.23       clasimpfile, axfile, hypsfile, probfile)]);*)
    5.24 -	 Watcher.callResProvers(childout,
    5.25 +  if !full_spass 
    5.26 +  then
    5.27 +   (Watcher.callResProvers(childout,
    5.28 +	    [("spass", thmstr, goalstring (*,spass_home*), 
    5.29 +	     getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",  
    5.30 +	     "-DocProof", 
    5.31 +	     clasimpfile, axfile, hypsfile, probfile)]))
    5.32 +  else	
    5.33 +   (Watcher.callResProvers(childout,
    5.34  	    [("spass", thmstr, goalstring (*,spass_home*), 
    5.35  	     getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell",  
    5.36  	     "-Auto=0%-ISRe%-ISFc%-RTaut%-RFSub%-RBSub%-DocProof", 
    5.37 -	     clasimpfile, axfile, hypsfile, probfile)]);
    5.38 +	     clasimpfile, axfile, hypsfile, probfile)]));
    5.39       
    5.40  	(* with paramodulation *)
    5.41  	(*Watcher.callResProvers(childout,
     6.1 --- a/src/HOL/Tools/res_axioms.ML	Tue May 31 12:36:01 2005 +0200
     6.2 +++ b/src/HOL/Tools/res_axioms.ML	Tue May 31 12:42:36 2005 +0200
     6.3 @@ -396,7 +396,19 @@
     6.4  
     6.5  (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****)
     6.6  
     6.7 -(* outputs a list of (thm,clause) pairs *)
     6.8 +(* outputs a list of (clause,thm) pairs *)
     6.9 +(*fun clausify_axiom_pairs (thm_name,thm) =
    6.10 +    let val isa_clauses = cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *)
    6.11 +        val isa_clauses' = rm_Eps [] isa_clauses
    6.12 +        val clauses_n = length isa_clauses
    6.13 +	fun make_axiom_clauses _ [] []= []
    6.14 +	  | make_axiom_clauses i (cls::clss) (cls'::clss')= ((ResClause.make_axiom_clause cls (thm_name,i)),cls', thm_name, i) :: make_axiom_clauses (i+1) clss clss'
    6.15 +    in
    6.16 +	make_axiom_clauses 0 isa_clauses' isa_clauses		
    6.17 +    end;
    6.18 +*)
    6.19 +
    6.20 +
    6.21  fun clausify_axiom_pairs (thm_name,thm) =
    6.22      let val isa_clauses = cnf_axiom (thm_name,thm) (*"isa_clauses" are already "standard"ed. *)
    6.23          val isa_clauses' = rm_Eps [] isa_clauses
    6.24 @@ -407,7 +419,6 @@
    6.25  	make_axiom_clauses 0 isa_clauses' isa_clauses		
    6.26      end;
    6.27  
    6.28 -
    6.29  fun clausify_rules_pairs [] err_list = ([],err_list)
    6.30    | clausify_rules_pairs ((name,thm)::thms) err_list =
    6.31      let val (ts,es) = clausify_rules_pairs thms err_list