A new structure and reduced indentation
authorpaulson
Tue May 24 10:23:24 2005 +0200 (2005-05-24)
changeset 160618a139c1557bf
parent 16060 833be7f71ecd
child 16062 f8110bd9957f
A new structure and reduced indentation
src/HOL/Tools/ATP/recon_order_clauses.ML
src/HOL/Tools/ATP/recon_parse.ML
src/HOL/Tools/ATP/recon_transfer_proof.ML
src/HOL/Tools/ATP/recon_translate_proof.ML
src/HOL/Tools/ATP/res_clasimpset.ML
src/HOL/Tools/ATP/watcher.ML
src/HOL/Tools/res_atp.ML
     1.1 --- a/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue May 24 07:43:38 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_order_clauses.ML	Tue May 24 10:23:24 2005 +0200
     1.3 @@ -3,6 +3,9 @@
     1.4      Copyright   2004  University of Cambridge
     1.5  *)
     1.6  
     1.7 +structure ReconOrderClauses =
     1.8 +struct
     1.9 +
    1.10  (*----------------------------------------------*)
    1.11  (* Reorder clauses for use in binary resolution *)
    1.12  (*----------------------------------------------*)
    1.13 @@ -21,8 +24,6 @@
    1.14  |   numlist n = (numlist (n - 1))@[n]
    1.15  
    1.16  
    1.17 -
    1.18 -
    1.19  fun last(x::xs) = if xs=[] then x else last xs
    1.20  fun butlast []= []
    1.21  |   butlast(x::xs) = if xs=[] then [] else (x::(butlast xs))
    1.22 @@ -38,21 +39,13 @@
    1.23                                  then
    1.24                                       (res, xs)
    1.25                                  else
    1.26 -                                     takeUntil ch xs (res@[x])
    1.27 +                                     takeUntil ch xs (res@[x]);
    1.28 +
    1.29  fun contains_eq str = inlist "=" str 
    1.30  
    1.31  fun eq_not_neq str = let val uptoeq = fst(takeUntil "=" str [])
    1.32 -                     in
    1.33 -                        if ((last uptoeq) = "~")
    1.34 -                        then 
    1.35 -                            false
    1.36 -                        else
    1.37 -                            true
    1.38 -                     end
    1.39 +                     in (last uptoeq) <> "~" end
    1.40                     
    1.41 -
    1.42 -
    1.43 -
    1.44  fun get_eq_strs str =  if eq_not_neq  str   (*not an inequality *)
    1.45                         then 
    1.46                             let val (left, right) = takeUntil "=" str []
    1.47 @@ -69,7 +62,6 @@
    1.48  
    1.49  fun switch_equal a x = let val (a_lhs, a_rhs) = get_eq_strs a
    1.50                             val (x_lhs, x_rhs) = get_eq_strs x
    1.51 -
    1.52                         in
    1.53                             (a_lhs = x_rhs) andalso (a_rhs = x_lhs)
    1.54                         end
    1.55 @@ -88,111 +80,107 @@
    1.56  
    1.57  
    1.58  
    1.59 -fun var_pos_eq vars x y = String.size x = String.size y andalso
    1.60 -			  let val xs = explode x
    1.61 -                              val ys = explode y
    1.62 -                              val xsys = ListPair.zip (xs,ys)
    1.63 -                              val are_var_pairs = map (var_equiv vars) xsys
    1.64 -                          in
    1.65 -                              all_true are_var_pairs 
    1.66 -                          end
    1.67 +fun var_pos_eq vars x y = 
    1.68 +    String.size x = String.size y andalso
    1.69 +    let val xs = explode x
    1.70 +	val ys = explode y
    1.71 +	val xsys = ListPair.zip (xs,ys)
    1.72 +	val are_var_pairs = map (var_equiv vars) xsys
    1.73 +    in
    1.74 +	all_true are_var_pairs 
    1.75 +    end;
    1.76 +
    1.77 +fun pos_in_list a [] allvars (pos_num, symlist, nsymlist) =  raise Not_in_list
    1.78 +  | pos_in_list a (x::[]) allvars (pos_num , symlist, nsymlist) = 
    1.79 +      let val y = explode x 
    1.80 +	  val b = explode a
    1.81 +      in
    1.82 +	 if  b = y
    1.83 +	 then 
    1.84 +	      (pos_num, symlist, nsymlist)
    1.85 +	 else 
    1.86 +	      if (var_pos_eq allvars  a x) 
    1.87 +	      then  (* Equal apart from meta-vars having different names *)
    1.88 +		  (pos_num, symlist, nsymlist)
    1.89 +	      else 
    1.90 +		  if (contains_eq b) andalso (contains_eq y)
    1.91 +		  then 
    1.92 +		      if (eq_not_neq b) andalso (eq_not_neq y)  andalso (switch_equal b y )          
    1.93 +		      then (* both are equalities and equal under sym*) 
    1.94 +			  (pos_num, (pos_num::symlist), nsymlist)  (* add pos to symlist *)                                                                    
    1.95 +			  else 
    1.96 +			  if not(eq_not_neq b) andalso not(eq_not_neq y) andalso  (switch_equal b y)
    1.97 +			   then (* if they're equal under not_sym *)
    1.98 +			       (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
    1.99 +			   else 
   1.100 +				raise Not_in_list
   1.101 +		  else 
   1.102 +		       raise Not_in_list
   1.103 +      end   
   1.104 +  | pos_in_list a (x::xs) allvars (pos_num, symlist, nsymlist) = 
   1.105 +      let val y = explode x 
   1.106 +	  val b = explode a
   1.107 +      in
   1.108 +	 if  b = y
   1.109 +	 then 
   1.110 +	      (pos_num, symlist, nsymlist)
   1.111 +	 
   1.112 +	 else
   1.113 +	       if (var_pos_eq allvars  a x) (* Equal apart from meta-vars having different names *)
   1.114 +	       then 
   1.115 +		  (pos_num, symlist, nsymlist)
   1.116 +	       else 
   1.117 +		   if (contains_eq b) andalso (contains_eq y)
   1.118 +		   then 
   1.119 +		       if (eq_not_neq b) andalso (eq_not_neq y)  andalso (switch_equal b y )   (* both are equalities and equal under sym*)        
   1.120 +		       then 
   1.121 +			   (pos_num, (pos_num::symlist), nsymlist)  (* add pos to symlist *)                                                                    else 
   1.122 +			   if not(eq_not_neq b) andalso not(eq_not_neq y) andalso  (switch_equal b y )  (* if they're equal under not_sym *)
   1.123 +			   then 
   1.124 +				(pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
   1.125 +			   else 
   1.126 +				pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
   1.127 +		   else 
   1.128 +			 pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
   1.129 +		   
   1.130 +      end;
   1.131  
   1.132  
   1.133 -fun  pos_in_list a [] allvars (pos_num, symlist, nsymlist) =  raise Not_in_list
   1.134 -    |pos_in_list a (x::[])  allvars (pos_num , symlist, nsymlist) = 
   1.135 -                                 let val y = explode x 
   1.136 -                                     val b = explode a
   1.137 -                                 in
   1.138 -                                    if  b = y
   1.139 -                                    then 
   1.140 -                                         (pos_num, symlist, nsymlist)
   1.141 -                                    else 
   1.142 -                                         if (var_pos_eq allvars  a x) (* Equal apart from meta-vars having different names *)
   1.143 -                                         then 
   1.144 -                                             (pos_num, symlist, nsymlist)
   1.145 -                                         else 
   1.146 -                                             if (contains_eq b) andalso (contains_eq y)
   1.147 -                                             then 
   1.148 -                                                 if (eq_not_neq b) andalso (eq_not_neq y)  andalso (switch_equal b y )   (* both are equalities and equal under sym*)        
   1.149 -                                                 then 
   1.150 -                                                     (pos_num, (pos_num::symlist), nsymlist)  (* add pos to symlist *)                                                                    else 
   1.151 -                                                      if not(eq_not_neq b) andalso not(eq_not_neq y) andalso  (switch_equal b y )  (* if they're equal under not_sym *)
   1.152 -                                                      then 
   1.153 -                                                          (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
   1.154 -                                                      else 
   1.155 -                                                           raise Not_in_list
   1.156 -                                             else 
   1.157 -                                                  raise Not_in_list
   1.158 -                                              
   1.159 -                                 end   
   1.160 -                                 
   1.161 -    | pos_in_list a (x::xs) allvars (pos_num, symlist, nsymlist) = 
   1.162 -                                 let val y = explode x 
   1.163 -                                     val b = explode a
   1.164 -                                 in
   1.165 -                                    if  b = y
   1.166 -                                    then 
   1.167 -                                         (pos_num, symlist, nsymlist)
   1.168 -                                    
   1.169 -                                    else
   1.170 -                                          if (var_pos_eq allvars  a x) (* Equal apart from meta-vars having different names *)
   1.171 -                                          then 
   1.172 -                                             (pos_num, symlist, nsymlist)
   1.173 -                                          else 
   1.174 -                                              if (contains_eq b) andalso (contains_eq y)
   1.175 -                                              then 
   1.176 -                                                  if (eq_not_neq b) andalso (eq_not_neq y)  andalso (switch_equal b y )   (* both are equalities and equal under sym*)        
   1.177 -                                                  then 
   1.178 -                                                      (pos_num, (pos_num::symlist), nsymlist)  (* add pos to symlist *)                                                                    else 
   1.179 -                                                      if not(eq_not_neq b) andalso not(eq_not_neq y) andalso  (switch_equal b y )  (* if they're equal under not_sym *)
   1.180 -                                                      then 
   1.181 -                                                           (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
   1.182 -                                                      else 
   1.183 -                                                           pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
   1.184 -                                              else 
   1.185 -                                                    pos_in_list a xs allvars((pos_num + 1), symlist, nsymlist)
   1.186 -                                              
   1.187 -                                 end   
   1.188 +    (* in
   1.189 +	if  b = y
   1.190 +	then 
   1.191 +	     (pos_num, symlist, nsymlist)
   1.192 +	else if (contains_eq b) andalso (contains_eq y)
   1.193 +	     then if (eq_not_neq b) andalso (eq_not_neq y) (* both are equalities*)
   1.194 +		  then if (switch_equal b y )              (* if they're equal under sym *)
   1.195 +		       then 
   1.196 +			   (pos_num, (pos_num::symlist), nsymlist)  (* add pos to symlist *)
   1.197 +		       else 
   1.198 +			     pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   1.199 +		  else if not(eq_not_neq b) andalso not(eq_not_neq y)  (* both are inequalities *)
   1.200 +		       then if (switch_equal b y )  (* if they're equal under not_sym *)
   1.201 +			    then 
   1.202 +				(pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
   1.203 +			    else 
   1.204 +				     pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   1.205 +		       else
   1.206 +			      pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   1.207 +		   else  
   1.208 +			   pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   1.209 +	      else 
   1.210 +		      pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   1.211 +     end   
   1.212  
   1.213 -
   1.214 -
   1.215 -
   1.216 -
   1.217 -
   1.218 -
   1.219 -                                (* in
   1.220 -                                    if  b = y
   1.221 -                                    then 
   1.222 -                                         (pos_num, symlist, nsymlist)
   1.223 -                                    else if (contains_eq b) andalso (contains_eq y)
   1.224 -                                         then if (eq_not_neq b) andalso (eq_not_neq y) (* both are equalities*)
   1.225 -                                              then if (switch_equal b y )              (* if they're equal under sym *)
   1.226 -                                                   then 
   1.227 -                                                       (pos_num, (pos_num::symlist), nsymlist)  (* add pos to symlist *)
   1.228 -                                                   else 
   1.229 -                                                         pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   1.230 -                                              else if not(eq_not_neq b) andalso not(eq_not_neq y)  (* both are inequalities *)
   1.231 -                                                   then if (switch_equal b y )  (* if they're equal under not_sym *)
   1.232 -                                                        then 
   1.233 -                                                            (pos_num, (symlist), (pos_num::nsymlist))(* add pos to nsymlist *)
   1.234 -                                                        else 
   1.235 -                                                                 pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   1.236 -                                                   else
   1.237 -                                                          pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   1.238 -                                               else  
   1.239 -                                                       pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   1.240 -                                          else 
   1.241 -                                                  pos_in_list a xs ((pos_num + 1), symlist, nsymlist)
   1.242 -                                 end   
   1.243 -
   1.244 -                                *)
   1.245 +    *)
   1.246  
   1.247  
   1.248  (* checkorder Spass Isabelle [] *)
   1.249  
   1.250 -fun checkorder [] strlist allvars (numlist, symlist, not_symlist)= (numlist,symlist, not_symlist)
   1.251 +fun checkorder [] strlist allvars (numlist, symlist, not_symlist) =
   1.252 +      (numlist,symlist, not_symlist)
   1.253  |   checkorder (x::xs) strlist allvars (numlist, symlist, not_symlist) =  
   1.254 -         let val (posnum, symlist', not_symlist') = pos_in_list x strlist allvars (0, symlist, not_symlist) 
   1.255 +         let val (posnum, symlist', not_symlist') = 
   1.256 +               pos_in_list x strlist allvars (0, symlist, not_symlist) 
   1.257           in
   1.258               checkorder xs  strlist allvars ((numlist@[posnum]), symlist', not_symlist') 
   1.259           end
   1.260 @@ -206,26 +194,28 @@
   1.261      (ch >=  "a" andalso ch <=  "z")
   1.262  
   1.263  
   1.264 -fun is_alpha_space_or_neg_or_eq ch = (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=")
   1.265 +fun is_alpha_space_or_neg_or_eq ch =
   1.266 +    (ch = "~") orelse (is_alpha ch) orelse ( ch = " ")orelse ( ch = "=")
   1.267  
   1.268  fun lit_string sg t = 
   1.269 -                   let val termstr = Sign.string_of_term sg t
   1.270 -                       val exp_term = explode termstr
   1.271 -                   in
   1.272 -                       implode(List.filter is_alpha_space_or_neg_or_eq exp_term)
   1.273 -                   end
   1.274 +    let val termstr = Sign.string_of_term sg t
   1.275 +	val exp_term = explode termstr
   1.276 +    in
   1.277 +	implode(List.filter is_alpha_space_or_neg_or_eq exp_term)
   1.278 +    end
   1.279  
   1.280  fun get_meta_lits thm = map (lit_string (sign_of_thm thm)) (prems_of thm)
   1.281  
   1.282  
   1.283 -fun is_alpha_space_or_neg_or_eq_or_bracket ch = is_alpha_space_or_neg_or_eq ch orelse (ch= "(") orelse (ch = ")")
   1.284 +fun is_alpha_space_or_neg_or_eq_or_bracket ch =
   1.285 +   is_alpha_space_or_neg_or_eq ch orelse (ch= "(") orelse (ch = ")")
   1.286  
   1.287  fun lit_string_bracket sg t = 
   1.288 -                   let val termstr = Sign.string_of_term sg t
   1.289 -                       val exp_term = explode termstr
   1.290 -                   in
   1.291 -                       implode(List.filter  is_alpha_space_or_neg_or_eq_or_bracket exp_term)
   1.292 -                   end
   1.293 +    let val termstr = Sign.string_of_term sg t
   1.294 +	val exp_term = explode termstr
   1.295 +    in
   1.296 +	implode(List.filter  is_alpha_space_or_neg_or_eq_or_bracket exp_term)
   1.297 +    end;
   1.298  
   1.299  fun get_meta_lits_bracket thm = 
   1.300      map (lit_string_bracket (sign_of_thm thm)) (prems_of thm)
   1.301 @@ -239,14 +229,17 @@
   1.302  
   1.303  
   1.304  
   1.305 -                    (* resulting thm, clause-strs in spass order, vars *)
   1.306 +(* resulting thm, clause-strs in spass order, vars *)
   1.307  
   1.308  fun rearrange_clause thm res_strlist allvars = 
   1.309 -                          let val isa_strlist = get_meta_lits thm (* change this to use Jia's code to get same looking thing as isastrlist? *)
   1.310 -                              val (posns, symlist, not_symlist) = checkorder res_strlist isa_strlist allvars([],[],[])
   1.311 -                              val symmed = apply_rule sym symlist thm
   1.312 -                              val not_symmed = apply_rule not_sym not_symlist symmed
   1.313 -                                           
   1.314 -                          in
   1.315 -                             ((rearrange_prems posns not_symmed), posns, symlist,not_symlist)
   1.316 -                          end
   1.317 +    let val isa_strlist = get_meta_lits thm 
   1.318 +        (* change this to use Jia's code to get same looking thing as isastrlist? *)
   1.319 +	val (posns, symlist, not_symlist) = checkorder res_strlist isa_strlist allvars([],[],[])
   1.320 +	val symmed = apply_rule sym symlist thm
   1.321 +	val not_symmed = apply_rule not_sym not_symlist symmed
   1.322 +    in
   1.323 +       ((rearrange_prems posns not_symmed), posns, symlist,not_symlist)
   1.324 +    end
   1.325 +    
   1.326 +end;
   1.327 +
     2.1 --- a/src/HOL/Tools/ATP/recon_parse.ML	Tue May 24 07:43:38 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_parse.ML	Tue May 24 10:23:24 2005 +0200
     2.3 @@ -436,23 +436,21 @@
     2.4                                       dropUntilNot ch xs
     2.5  
     2.6  
     2.7 -
     2.8 -
     2.9 -
    2.10  fun remove_spaces str  []  = str
    2.11  |   remove_spaces str (x::[]) = if x = " " 
    2.12                                  then 
    2.13                                      str 
    2.14                                  else 
    2.15                                      (str^x)
    2.16 -|   remove_spaces str (x::xs) = let val (first, rest) = takeUntil " " (x::xs) []
    2.17 -                                    val (next) = dropUntilNot " " rest 
    2.18 -                                in 
    2.19 -                                    if next = []
    2.20 -                                    then 
    2.21 -                                         (str^(implode first)) 
    2.22 -                                    else remove_spaces  (str^(implode first)^" ") next 
    2.23 -                                end
    2.24 +|   remove_spaces str (x::xs) = 
    2.25 +      let val (first, rest) = ReconOrderClauses.takeUntil " " (x::xs) []
    2.26 +	  val (next) = dropUntilNot " " rest 
    2.27 +      in 
    2.28 +	  if next = []
    2.29 +	  then 
    2.30 +	       (str^(implode first)) 
    2.31 +	  else remove_spaces  (str^(implode first)^" ") next 
    2.32 +      end
    2.33  
    2.34  
    2.35  fun remove_space_strs clsstrs = map (remove_spaces "") (map explode clsstrs)
    2.36 @@ -461,25 +459,25 @@
    2.37  fun all_spaces xs = List.filter  (not_equal " " ) xs
    2.38  
    2.39  fun just_change_space []  = []
    2.40 -|   just_change_space ((clausenum, step, strs)::xs) = let val newstrs = remove_space_strs strs
    2.41 -                                                 in
    2.42 -                                                    if (all_spaces newstrs = [] ) (* all type_info *)                                                    then    
    2.43 -                                                       (clausenum, step, newstrs)::(just_change_space xs)
    2.44 -                                                    else 
    2.45 -                                                        (clausenum, step, newstrs)::(just_change_space xs) 
    2.46 -                                                 end
    2.47 -
    2.48 -
    2.49 -
    2.50 +|   just_change_space ((clausenum, step, strs)::xs) =
    2.51 +      let val newstrs = remove_space_strs strs
    2.52 +      in
    2.53 +	 if (all_spaces newstrs = [] ) (* all type_info *)
    2.54 +	 then    
    2.55 +	    (clausenum, step, newstrs)::(just_change_space xs)
    2.56 +	 else 
    2.57 +	     (clausenum, step, newstrs)::(just_change_space xs) 
    2.58 +      end;
    2.59  
    2.60  fun change_space []  = []
    2.61 -|   change_space ((clausenum, step, strs)::xs) = let val newstrs = remove_space_strs strs
    2.62 -                                                 in
    2.63 -                                                    if (all_spaces newstrs = [] ) (* all type_info *)
    2.64 -                                                    then    
    2.65 -                                                       (clausenum, step, T_info, newstrs)::(change_space xs)
    2.66 -                                                    else 
    2.67 -                                                        (clausenum, step, P_info, newstrs)::(change_space xs) 
    2.68 -                                                 end
    2.69 +|   change_space ((clausenum, step, strs)::xs) = 
    2.70 +      let val newstrs = remove_space_strs strs
    2.71 +      in
    2.72 +	 if (all_spaces newstrs = [] ) (* all type_info *)
    2.73 +	 then    
    2.74 +	    (clausenum, step, T_info, newstrs)::(change_space xs)
    2.75 +	 else 
    2.76 +	     (clausenum, step, P_info, newstrs)::(change_space xs) 
    2.77 +      end
    2.78  
    2.79  end;
     3.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue May 24 07:43:38 2005 +0200
     3.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue May 24 10:23:24 2005 +0200
     3.3 @@ -107,10 +107,13 @@
     3.4  
     3.5  (*** get a string representing the Isabelle ordered axioms ***)
     3.6  
     3.7 -fun origAx_to_string (num,(meta,thmvars)) =let val clause_strs = get_meta_lits_bracket meta
     3.8 -                                         in
     3.9 -                                            (string_of_int num)^"OrigAxiom()"^"["^(clause_strs_to_string clause_strs "")^"]"^"["^(thmvars_to_string thmvars "")^"]"
    3.10 -                                         end
    3.11 +fun origAx_to_string (num,(meta,thmvars)) =
    3.12 +    let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta
    3.13 +    in
    3.14 +       (string_of_int num)^"OrigAxiom()"^"["^
    3.15 +       (clause_strs_to_string clause_strs "")^"]"^"["^
    3.16 +       (thmvars_to_string thmvars "")^"]"
    3.17 +    end
    3.18  
    3.19  
    3.20  fun  origAxs_to_string [] str = str
    3.21 @@ -122,20 +125,20 @@
    3.22  
    3.23  (*** get a string representing the Isabelle ordered axioms not used in the spass proof***)
    3.24  
    3.25 -fun extraAx_to_string (num, (meta,thmvars)) = let val clause_strs = get_meta_lits_bracket meta
    3.26 -                                           in
    3.27 -                                              (string_of_int num)^"ExtraAxiom()"^"["^(clause_strs_to_string clause_strs "")^"]"^"["^(thmvars_to_string thmvars "")^"]"
    3.28 -                                           end
    3.29 -
    3.30 -
    3.31 +fun extraAx_to_string (num, (meta,thmvars)) =
    3.32 +   let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta
    3.33 +   in
    3.34 +      (string_of_int num)^"ExtraAxiom()"^"["^
    3.35 +      (clause_strs_to_string clause_strs "")^"]"^
    3.36 +      "["^(thmvars_to_string thmvars "")^"]"
    3.37 +   end;
    3.38  
    3.39 -fun  extraAxs_to_string [] str = str
    3.40 -|   extraAxs_to_string (x::xs) str = let val newstr = extraAx_to_string x 
    3.41 -                                   in
    3.42 -                                       extraAxs_to_string xs (str^newstr)
    3.43 -                                   end
    3.44 -
    3.45 -
    3.46 +fun extraAxs_to_string [] str = str
    3.47 +|   extraAxs_to_string (x::xs) str =
    3.48 +      let val newstr = extraAx_to_string x 
    3.49 +      in
    3.50 +	  extraAxs_to_string xs (str^newstr)
    3.51 +      end;
    3.52  
    3.53  fun is_axiom ( num:int,Axiom, str) = true
    3.54  |   is_axiom (num, _,_) = false
    3.55 @@ -156,7 +159,7 @@
    3.56  |   get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))])
    3.57  *)
    3.58  (*FIX - should this have vars in it? *)
    3.59 -fun there_out_of_order xs ys = (checkorder xs ys [] ([],[],[]); true) 
    3.60 +fun there_out_of_order xs ys = (ReconOrderClauses.checkorder xs ys [] ([],[],[]); true) 
    3.61                                 handle _ => false
    3.62  
    3.63  fun assoc_out_of_order a [] = raise Noassoc
    3.64 @@ -202,94 +205,94 @@
    3.65  (* add array and table here, so can retrieve clasimp axioms *)
    3.66  
    3.67   fun get_axioms_used proof_steps thms clause_arr num_of_clauses  =
    3.68 -                                         let 
    3.69 -                                             (*val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
    3.70 -                                             val _ = TextIO.output (outfile, thmstring)
    3.71 -                                             
    3.72 -                                             val _ =  TextIO.closeOut outfile*)
    3.73 -                                            (* not sure why this is necessary again, but seems to be *)
    3.74 +     let 
    3.75 +	 (*val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
    3.76 +	 val _ = TextIO.output (outfile, thmstring)
    3.77 +	 
    3.78 +	 val _ =  TextIO.closeOut outfile*)
    3.79 +	(* not sure why this is necessary again, but seems to be *)
    3.80  
    3.81 -                                            val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    3.82 -                                            val axioms = get_init_axioms proof_steps
    3.83 -                                            val step_nums = get_step_nums axioms []
    3.84 +	val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    3.85 +	val axioms = get_init_axioms proof_steps
    3.86 +	val step_nums = get_step_nums axioms []
    3.87  
    3.88 -                                           (***********************************************)
    3.89 -                                           (* here need to add the clauses from clause_arr*)
    3.90 -                                           (***********************************************)
    3.91 +       (***********************************************)
    3.92 +       (* here need to add the clauses from clause_arr*)
    3.93 +       (***********************************************)
    3.94  
    3.95 -                                           (* val clasimp_names_cls = get_clasimp_cls clause_arr   num_of_clauses step_nums   
    3.96 -                                            val clasimp_names = map #1 clasimp_names_cls
    3.97 -                                            val clasimp_cls = map #2 clasimp_names_cls
    3.98 -                                            val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "clasimp_names")))                                                            val clasimp_namestr = concat clasimp_names                            
    3.99 -                                             val _ = TextIO.output (outfile,clasimp_namestr)
   3.100 -                                             
   3.101 -                                             val _ =  TextIO.closeOut outfile
   3.102 +       (* val clasimp_names_cls = get_clasimp_cls clause_arr   num_of_clauses step_nums   
   3.103 +	val clasimp_names = map #1 clasimp_names_cls
   3.104 +	val clasimp_cls = map #2 clasimp_names_cls
   3.105 +	val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "clasimp_names")))                                                            val clasimp_namestr = concat clasimp_names                            
   3.106 +	 val _ = TextIO.output (outfile,clasimp_namestr)
   3.107 +	 
   3.108 +	 val _ =  TextIO.closeOut outfile
   3.109  *)
   3.110  
   3.111 -                                            val clauses =(*(clasimp_cls)@*)( make_clauses thms)
   3.112 -                                            
   3.113 -                                            val vars = map thm_vars clauses
   3.114 -                                           
   3.115 -                                            val distvars = distinct (fold append vars [])
   3.116 -                                            val clause_terms = map prop_of clauses  
   3.117 -                                            val clause_frees = List.concat (map term_frees clause_terms)
   3.118 +	val clauses =(*(clasimp_cls)@*)( make_clauses thms)
   3.119 +	
   3.120 +	val vars = map thm_vars clauses
   3.121 +       
   3.122 +	val distvars = distinct (fold append vars [])
   3.123 +	val clause_terms = map prop_of clauses  
   3.124 +	val clause_frees = List.concat (map term_frees clause_terms)
   3.125  
   3.126 -                                            val frees = map lit_string_with_nums clause_frees;
   3.127 +	val frees = map lit_string_with_nums clause_frees;
   3.128  
   3.129 -                                            val distfrees = distinct frees
   3.130 +	val distfrees = distinct frees
   3.131  
   3.132 -                                            val metas = map Meson.make_meta_clause clauses
   3.133 -                                            val ax_strs = map #3 axioms
   3.134 +	val metas = map Meson.make_meta_clause clauses
   3.135 +	val ax_strs = map #3 axioms
   3.136  
   3.137 -                                            (* literals of -all- axioms, not just those used by spass *)
   3.138 -                                            val meta_strs = map get_meta_lits metas
   3.139 -                                           
   3.140 -                                            val metas_and_strs = ListPair.zip (metas,meta_strs)
   3.141 -                                             val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses")));                                                                       
   3.142 -                                             val _ = TextIO.output (outfile, onestr ax_strs)
   3.143 -                                             
   3.144 -                                             val _ =  TextIO.closeOut outfile
   3.145 -                                             val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metastrs")));                                                                       
   3.146 -                                             val _ = TextIO.output (outfile, onestr meta_strs)
   3.147 -                                             val _ =  TextIO.closeOut outfile
   3.148 +	(* literals of -all- axioms, not just those used by spass *)
   3.149 +	val meta_strs = map ReconOrderClauses.get_meta_lits metas
   3.150 +       
   3.151 +	val metas_and_strs = ListPair.zip (metas,meta_strs)
   3.152 +	 val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_clauses")));                                                                       
   3.153 +	 val _ = TextIO.output (outfile, onestr ax_strs)
   3.154 +	 
   3.155 +	 val _ =  TextIO.closeOut outfile
   3.156 +	 val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metastrs")));                                                                       
   3.157 +	 val _ = TextIO.output (outfile, onestr meta_strs)
   3.158 +	 val _ =  TextIO.closeOut outfile
   3.159  
   3.160 -                                            (* get list of axioms as thms with their variables *)
   3.161 +	(* get list of axioms as thms with their variables *)
   3.162  
   3.163 -                                            val ax_metas = get_assoc_snds ax_strs metas_and_strs []
   3.164 -                                            val ax_vars = map thm_vars ax_metas
   3.165 -                                            val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
   3.166 +	val ax_metas = get_assoc_snds ax_strs metas_and_strs []
   3.167 +	val ax_vars = map thm_vars ax_metas
   3.168 +	val ax_with_vars = ListPair.zip (ax_metas,ax_vars)
   3.169  
   3.170 -                                            (* get list of extra axioms as thms with their variables *)
   3.171 -                                            val extra_metas = add_if_not_inlist metas ax_metas []
   3.172 -                                            val extra_vars = map thm_vars extra_metas
   3.173 -                                            val extra_with_vars = if (not (extra_metas = []) ) 
   3.174 -                                                                  then
   3.175 - 									 ListPair.zip (extra_metas,extra_vars)
   3.176 -                                                                  else
   3.177 -                                                                         []
   3.178 +	(* get list of extra axioms as thms with their variables *)
   3.179 +	val extra_metas = add_if_not_inlist metas ax_metas []
   3.180 +	val extra_vars = map thm_vars extra_metas
   3.181 +	val extra_with_vars = if (not (extra_metas = []) ) 
   3.182 +			      then
   3.183 +				     ListPair.zip (extra_metas,extra_vars)
   3.184 +			      else
   3.185 +				     []
   3.186  
   3.187 -                                           (* val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   3.188 -                                           val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metas")))
   3.189 +       (* val _=  (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
   3.190 +       val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_metas")))
   3.191  
   3.192 -                                           val _ = TextIO.output (outfile, ((thmstrings ax_metas "")))
   3.193 -                                           val _ =  TextIO.closeOut outfile
   3.194 -                                          val foo_metas =  File.sysify_path(File.tmp_path (Path.basic "foo_metas"))
   3.195 -                                          val foo_metas2 =   File.sysify_path(File.tmp_path (Path.basic "foo_metas2"))
   3.196 -                                            val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", "  <", foo_metas, "  >", foo_metas2])
   3.197 -                                         val infile = TextIO.openIn(File.sysify_path(File.tmp_path (Path.basic "foo_metas2")))
   3.198 -                                        val ax_metas_str = TextIO.inputLine (infile)
   3.199 -                                        val _ = TextIO.closeIn infile
   3.200 -                                           val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
   3.201 -                                           
   3.202 -                                         in
   3.203 -                                            (distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas)))
   3.204 -                                         end
   3.205 -                                        
   3.206 +       val _ = TextIO.output (outfile, ((thmstrings ax_metas "")))
   3.207 +       val _ =  TextIO.closeOut outfile
   3.208 +      val foo_metas =  File.sysify_path(File.tmp_path (Path.basic "foo_metas"))
   3.209 +      val foo_metas2 =   File.sysify_path(File.tmp_path (Path.basic "foo_metas2"))
   3.210 +	val execperl = Unix.execute("/usr/bin/perl", ["remchars.pl", "  <", foo_metas, "  >", foo_metas2])
   3.211 +     val infile = TextIO.openIn(File.sysify_path(File.tmp_path (Path.basic "foo_metas2")))
   3.212 +    val ax_metas_str = TextIO.inputLine (infile)
   3.213 +    val _ = TextIO.closeIn infile
   3.214 +       val _= (print_mode := (["xsymbols", "symbols"] @ ! print_mode))*)
   3.215 +       
   3.216 +     in
   3.217 +	(distfrees,distvars, extra_with_vars,ax_with_vars, (*clasimp_names*)(ListPair.zip (step_nums,ax_metas)))
   3.218 +     end
   3.219 +    
   3.220  fun numclstr (vars, []) str = str
   3.221  |   numclstr ( vars, ((num, thm)::rest)) str = let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" "
   3.222 -                               in
   3.223 -                                   numclstr  (vars,rest) newstr
   3.224 -                               end
   3.225 +in
   3.226 +numclstr  (vars,rest) newstr
   3.227 +end
   3.228  
   3.229  (*
   3.230  
   3.231 @@ -366,101 +369,101 @@
   3.232  val dummy_tac = PRIMITIVE(fn thm => thm );
   3.233  
   3.234  fun spassString_to_reconString proofstr thmstring goalstring toParent ppid thms clause_arr  num_of_clauses  = 
   3.235 -                                              let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));                                        
   3.236 -                                                  (* val sign = sign_of_thm thm
   3.237 -                                                 val prems = prems_of thm
   3.238 -                                                 val prems_string =  concat_with_and (map (Sign.string_of_term sign) prems) "" 
   3.239 -                                                  val _ = warning ("thmstring is: "^thmstring);(*("thm in spassStrtoRec: "^(concat_with_and (map string_of_thm thms) "")^*)*)
   3.240 -                                                  val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr))
   3.241 -             (*val _ = TextIO.output (outfile, (("in spassStrto Reconstr")));*)
   3.242 -                                                  val _ =  TextIO.closeOut outfile
   3.243 +      let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thmstringfile")));                                        
   3.244 +	  (* val sign = sign_of_thm thm
   3.245 +	 val prems = prems_of thm
   3.246 +	 val prems_string =  concat_with_and (map (Sign.string_of_term sign) prems) "" 
   3.247 +	  val _ = warning ("thmstring is: "^thmstring);(*("thm in spassStrtoRec: "^(concat_with_and (map string_of_thm thms) "")^*)*)
   3.248 +	  val _ = TextIO.output (outfile, (" thmstring is: "^thmstring^"proofstr is: "^proofstr))
   3.249 +(*val _ = TextIO.output (outfile, (("in spassStrto Reconstr")));*)
   3.250 +	  val _ =  TextIO.closeOut outfile
   3.251  
   3.252 -                                                  val tokens = #1(lex proofstr)
   3.253 +	  val tokens = #1(lex proofstr)
   3.254  
   3.255 -                                                    
   3.256 +	    
   3.257  
   3.258 -                                              (***********************************)
   3.259 -                                              (* parse spass proof into datatype *)
   3.260 -                                              (***********************************)
   3.261 +      (***********************************)
   3.262 +      (* parse spass proof into datatype *)
   3.263 +      (***********************************)
   3.264  
   3.265 -                                                  val proof_steps1 = parse tokens
   3.266 -                                                  val proof_steps = just_change_space proof_steps1
   3.267 +	  val proof_steps1 = parse tokens
   3.268 +	  val proof_steps = just_change_space proof_steps1
   3.269  
   3.270 -                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse")));                                                                                          val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   3.271 -                                                  val _ =  TextIO.closeOut outfile
   3.272 -                                                
   3.273 -                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thmstring_at_parse")));                                                                             val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
   3.274 -                                                  val _ =  TextIO.closeOut outfile
   3.275 -                                              (************************************)
   3.276 -                                              (* recreate original subgoal as thm *)
   3.277 -                                              (************************************)
   3.278 -                                                
   3.279 -                                                  (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   3.280 -                                                  (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
   3.281 -                                                  (* subgoal this is, and turn it into meta_clauses *)
   3.282 -                                                  (* should prob add array and table here, so that we can get axioms*)
   3.283 -                                                  (* produced from the clasimpset rather than the problem *)
   3.284 -                                                  val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr  num_of_clauses
   3.285 -                                                  
   3.286 -                                                  (*val numcls_string = numclstr ( vars, numcls) ""*)
   3.287 -                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_axiom")));                                                                            val _ = TextIO.output (outfile,"got axioms")
   3.288 -                                                  val _ =  TextIO.closeOut outfile
   3.289 -                                                    
   3.290 -                                              (************************************)
   3.291 -                                              (* translate proof                  *)
   3.292 -                                              (************************************)
   3.293 -                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_steps")));                                                          val _ = TextIO.output (outfile, ("about to translate proof, steps: "^(init_proofsteps_to_string proof_steps "")))
   3.294 -                                                  val _ =  TextIO.closeOut outfile
   3.295 -                                                  val (newthm,proof) = translate_proof numcls  proof_steps vars
   3.296 -                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_steps2")));                                                                         val _ = TextIO.output (outfile, ("translated proof, steps: "^(init_proofsteps_to_string proof_steps "")))
   3.297 -                                                  val _ =  TextIO.closeOut outfile
   3.298 -                                              (***************************************************)
   3.299 -                                              (* transfer necessary steps as strings to Isabelle *)
   3.300 -                                              (***************************************************)
   3.301 -                                                  (* turn the proof into a string *)
   3.302 -                                                  val reconProofStr = proofs_to_string proof ""
   3.303 -                                                  (* do the bit for the Isabelle ordered axioms at the top *)
   3.304 -                                                  val ax_nums = map #1 numcls
   3.305 -                                                  val ax_strs = map get_meta_lits_bracket (map #2 numcls)
   3.306 -                                                  val numcls_strs = ListPair.zip (ax_nums,ax_strs)
   3.307 -                                                  val num_cls_vars =  map (addvars vars) numcls_strs;
   3.308 -                                                  val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) ""
   3.309 -                                                  
   3.310 -                                                  val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else []
   3.311 -                                                  val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
   3.312 -                                                  val frees_str = "["^(thmvars_to_string frees "")^"]"
   3.313 -                                                  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "reconstringfile")));
   3.314 +	  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_parse")));                                                                                          val _ = TextIO.output (outfile, ("Did parsing on "^proofstr))
   3.315 +	  val _ =  TextIO.closeOut outfile
   3.316 +	
   3.317 +	  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_thmstring_at_parse")));                                                                             val _ = TextIO.output (outfile, ("Parsing for thmstring: "^thmstring))
   3.318 +	  val _ =  TextIO.closeOut outfile
   3.319 +      (************************************)
   3.320 +      (* recreate original subgoal as thm *)
   3.321 +      (************************************)
   3.322 +	
   3.323 +	  (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
   3.324 +	  (* need to get prems_of thm, then get right one of the prems, relating to whichever*)
   3.325 +	  (* subgoal this is, and turn it into meta_clauses *)
   3.326 +	  (* should prob add array and table here, so that we can get axioms*)
   3.327 +	  (* produced from the clasimpset rather than the problem *)
   3.328 +	  val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr  num_of_clauses
   3.329 +	  
   3.330 +	  (*val numcls_string = numclstr ( vars, numcls) ""*)
   3.331 +	  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_axiom")));                                                                            val _ = TextIO.output (outfile,"got axioms")
   3.332 +	  val _ =  TextIO.closeOut outfile
   3.333 +	    
   3.334 +      (************************************)
   3.335 +      (* translate proof                  *)
   3.336 +      (************************************)
   3.337 +	  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_steps")));                                                          val _ = TextIO.output (outfile, ("about to translate proof, steps: "^(init_proofsteps_to_string proof_steps "")))
   3.338 +	  val _ =  TextIO.closeOut outfile
   3.339 +	  val (newthm,proof) = translate_proof numcls  proof_steps vars
   3.340 +	  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_steps2")));                                                                         val _ = TextIO.output (outfile, ("translated proof, steps: "^(init_proofsteps_to_string proof_steps "")))
   3.341 +	  val _ =  TextIO.closeOut outfile
   3.342 +      (***************************************************)
   3.343 +      (* transfer necessary steps as strings to Isabelle *)
   3.344 +      (***************************************************)
   3.345 +	  (* turn the proof into a string *)
   3.346 +	  val reconProofStr = proofs_to_string proof ""
   3.347 +	  (* do the bit for the Isabelle ordered axioms at the top *)
   3.348 +	  val ax_nums = map #1 numcls
   3.349 +	  val ax_strs = map ReconOrderClauses.get_meta_lits_bracket (map #2 numcls)
   3.350 +	  val numcls_strs = ListPair.zip (ax_nums,ax_strs)
   3.351 +	  val num_cls_vars =  map (addvars vars) numcls_strs;
   3.352 +	  val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) ""
   3.353 +	  
   3.354 +	  val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) else []
   3.355 +	  val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) ""
   3.356 +	  val frees_str = "["^(thmvars_to_string frees "")^"]"
   3.357 +	  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "reconstringfile")));
   3.358  
   3.359 -                                                  val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr))
   3.360 -                                                  val _ =  TextIO.closeOut outfile
   3.361 -    						  val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
   3.362 -                                              in 
   3.363 -                                                   TextIO.output (toParent, reconstr^"\n");
   3.364 -                                                   TextIO.flushOut toParent;
   3.365 -                                        	   TextIO.output (toParent, thmstring^"\n");
   3.366 -                                         	   TextIO.flushOut toParent;
   3.367 -                                         	   TextIO.output (toParent, goalstring^"\n");
   3.368 -                                         	   TextIO.flushOut toParent;
   3.369 -                                          
   3.370 -                                         	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   3.371 -                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
   3.372 -                                         	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   3.373 -                                              end
   3.374 -                                              handle _ => (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
   3.375 +	  val _ = TextIO.output (outfile, (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr))
   3.376 +	  val _ =  TextIO.closeOut outfile
   3.377 +	  val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr)
   3.378 +      in 
   3.379 +	   TextIO.output (toParent, reconstr^"\n");
   3.380 +	   TextIO.flushOut toParent;
   3.381 +	   TextIO.output (toParent, thmstring^"\n");
   3.382 +	   TextIO.flushOut toParent;
   3.383 +	   TextIO.output (toParent, goalstring^"\n");
   3.384 +	   TextIO.flushOut toParent;
   3.385 +  
   3.386 +	   Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   3.387 +	  (* Attempt to prevent several signals from turning up simultaneously *)
   3.388 +	   Posix.Process.sleep(Time.fromSeconds 1) ; dummy_tac
   3.389 +      end
   3.390 +      handle _ => (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_handler")));
   3.391  
   3.392 -                                                  val _ = TextIO.output (outfile, ("In exception handler"));
   3.393 -                                                  val _ =  TextIO.closeOut outfile
   3.394 -                                              in 
   3.395 -                                                  TextIO.output (toParent,"Proof found but translation failed!" ^"\n");
   3.396 -                                                  TextIO.flushOut toParent;
   3.397 -						TextIO.output (toParent, thmstring^"\n");
   3.398 -                                         	   TextIO.flushOut toParent;
   3.399 -                                         	   TextIO.output (toParent, goalstring^"\n");
   3.400 -                                         	   TextIO.flushOut toParent;
   3.401 -            					  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   3.402 -                                         	  (* Attempt to prevent several signals from turning up simultaneously *)
   3.403 -                                         	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   3.404 -                                              end)
   3.405 +	  val _ = TextIO.output (outfile, ("In exception handler"));
   3.406 +	  val _ =  TextIO.closeOut outfile
   3.407 +      in 
   3.408 +	  TextIO.output (toParent,"Proof found but translation failed!" ^"\n");
   3.409 +	  TextIO.flushOut toParent;
   3.410 +	TextIO.output (toParent, thmstring^"\n");
   3.411 +	   TextIO.flushOut toParent;
   3.412 +	   TextIO.output (toParent, goalstring^"\n");
   3.413 +	   TextIO.flushOut toParent;
   3.414 +	  Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
   3.415 +	  (* Attempt to prevent several signals from turning up simultaneously *)
   3.416 +	  Posix.Process.sleep(Time.fromSeconds 1) ;dummy_tac
   3.417 +      end)
   3.418  
   3.419  
   3.420  
   3.421 @@ -742,9 +745,9 @@
   3.422                             val axioms = get_axioms axioms_and_steps
   3.423                             
   3.424                             val steps = Library.drop (origax_num, axioms_and_steps)
   3.425 -                           val firststeps = butlast steps
   3.426 -                           val laststep = last steps
   3.427 -                           val goalstring = implode(butlast(explode goalstring))
   3.428 +                           val firststeps = ReconOrderClauses.butlast steps
   3.429 +                           val laststep = ReconOrderClauses.last steps
   3.430 +                           val goalstring = implode(ReconOrderClauses.butlast(explode goalstring))
   3.431                          
   3.432                             val isar_proof = 
   3.433                             ("show \""^goalstring^"\"\n")^
     4.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Tue May 24 07:43:38 2005 +0200
     4.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Tue May 24 10:23:24 2005 +0200
     4.3 @@ -55,8 +55,9 @@
     4.4                       |P_info
     4.5  
     4.6  
     4.7 -fun is_alpha_space_digit_or_neg ch = (ch = "~") orelse (is_alpha ch) orelse (is_digit ch) orelse ( ch = " ")
     4.8 -
     4.9 +fun is_alpha_space_digit_or_neg ch =
    4.10 +    (ch = "~") orelse (ReconOrderClauses.is_alpha ch) orelse 
    4.11 +    (ReconOrderClauses.is_digit ch) orelse ( ch = " ");
    4.12  
    4.13  
    4.14  fun lit_string_with_nums t = let val termstr = Term.string_of_term t
    4.15 @@ -73,30 +74,29 @@
    4.16  (************************************************)
    4.17  
    4.18  fun follow_axiom clauses  allvars (clausenum:int) thml clause_strs =  
    4.19 -                                     let val this_axiom = valOf (assoc (clauses,clausenum))
    4.20 -                                         val (res, numlist, symlist, nsymlist) = (rearrange_clause this_axiom clause_strs allvars)         
    4.21 -                                         val thmvars = thm_vars res
    4.22 -                                     in
    4.23 -                                         (res, (Axiom,clause_strs,thmvars )  )
    4.24 -                                     end
    4.25 -                                     handle Option => reconstruction_failed "follow_axiom"
    4.26 +    let val this_axiom = valOf (assoc (clauses,clausenum))
    4.27 +	val (res, numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause this_axiom clause_strs allvars)         
    4.28 +	val thmvars = thm_vars res
    4.29 +    in
    4.30 +	(res, (Axiom,clause_strs,thmvars )  )
    4.31 +    end
    4.32 +    handle Option => reconstruction_failed "follow_axiom"
    4.33  
    4.34  (****************************************)
    4.35  (* Reconstruct a binary resolution step *)
    4.36  (****************************************)
    4.37  
    4.38                   (* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *)
    4.39 -fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs 
    4.40 -        = let
    4.41 -              val thm1 =  select_literal (lit1 + 1) (valOf (assoc (thml,clause1)))
    4.42 -              val thm2 =  valOf (assoc (thml,clause2))
    4.43 -              val res =   thm1 RSN ((lit2 +1), thm2)
    4.44 -              val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
    4.45 -              val thmvars = thm_vars res
    4.46 -          in
    4.47 -             (res',  ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) )
    4.48 -          end
    4.49 -	  handle Option => reconstruction_failed "follow_binary"
    4.50 +fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs =
    4.51 +    let val thm1 =  select_literal (lit1 + 1) (valOf (assoc (thml,clause1)))
    4.52 +	val thm2 =  valOf (assoc (thml,clause2))
    4.53 +	val res =   thm1 RSN ((lit2 +1), thm2)
    4.54 +	val (res', numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause res clause_strs allvars)
    4.55 +	val thmvars = thm_vars res
    4.56 +    in
    4.57 +       (res',  ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) )
    4.58 +    end
    4.59 +    handle Option => reconstruction_failed "follow_binary"
    4.60  
    4.61  
    4.62  
    4.63 @@ -105,17 +105,17 @@
    4.64  (******************************************************)
    4.65  
    4.66  
    4.67 -fun follow_mrr ((clause1, lit1), (clause2 , lit2))  allvars thml clause_strs 
    4.68 -        = let
    4.69 -              val thm1 =  select_literal (lit1 + 1) (valOf (assoc (thml,clause1)))
    4.70 -              val thm2 =  valOf (assoc (thml,clause2))
    4.71 -              val res =   thm1 RSN ((lit2 +1), thm2)
    4.72 -              val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
    4.73 -              val thmvars = thm_vars res
    4.74 -          in
    4.75 -             (res',  ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars))
    4.76 -          end
    4.77 -	  handle Option => reconstruction_failed "follow_mrr"
    4.78 +fun follow_mrr ((clause1, lit1), (clause2 , lit2))  allvars thml clause_strs =
    4.79 +    let val thm1 =  select_literal (lit1 + 1) (valOf (assoc (thml,clause1)))
    4.80 +	val thm2 =  valOf (assoc (thml,clause2))
    4.81 +	val res =   thm1 RSN ((lit2 +1), thm2)
    4.82 +	val (res', numlist, symlist, nsymlist) = 
    4.83 +	    (ReconOrderClauses.rearrange_clause res clause_strs allvars)
    4.84 +	val thmvars = thm_vars res
    4.85 +    in
    4.86 +       (res',  ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars))
    4.87 +    end
    4.88 +    handle Option => reconstruction_failed "follow_mrr"
    4.89  
    4.90  
    4.91  (*******************************************)
    4.92 @@ -123,11 +123,13 @@
    4.93  (*******************************************)
    4.94  
    4.95  fun mksubstlist [] sublist = sublist
    4.96 -   |mksubstlist ((a, (_, b)) :: rest) sublist = let val vartype = type_of b 
    4.97 -                                          val avar = Var(a,vartype)
    4.98 -                                          val newlist = ((avar,b)::sublist) in
    4.99 -                                          mksubstlist rest newlist
   4.100 -                                      end;
   4.101 +   |mksubstlist ((a, (_, b)) :: rest) sublist = 
   4.102 +       let val vartype = type_of b 
   4.103 +	   val avar = Var(a,vartype)
   4.104 +	   val newlist = ((avar,b)::sublist)
   4.105 +       in
   4.106 +	   mksubstlist rest newlist
   4.107 +       end;
   4.108  
   4.109  (* based on Tactic.distinct_subgoals_tac *)
   4.110  
   4.111 @@ -135,7 +137,7 @@
   4.112      let val (frozth,thawfn) = freeze_thaw state
   4.113          val froz_prems = cprems_of frozth
   4.114          val assumed = implies_elim_list frozth (map assume froz_prems)
   4.115 -        val new_prems = remove_nth lit froz_prems
   4.116 +        val new_prems = ReconOrderClauses.remove_nth lit froz_prems
   4.117          val implied = implies_intr_list new_prems assumed
   4.118      in  
   4.119          Seq.single (thawfn implied)  
   4.120 @@ -150,44 +152,46 @@
   4.121  (*************************************)
   4.122  
   4.123  (*FIXME: share code with that in Tools/reconstruction.ML*)
   4.124 -fun follow_factor clause lit1 lit2 allvars thml clause_strs= 
   4.125 -                          let 
   4.126 -                            val th =  valOf (assoc (thml,clause))
   4.127 -                            val prems = prems_of th
   4.128 -                            val sign = sign_of_thm th
   4.129 -                            val fac1 = get_nth (lit1+1) prems
   4.130 -                            val fac2 = get_nth (lit2+1) prems
   4.131 -                            val unif_env = Unify.unifiers (sign,Envir.empty 0, [(fac1, fac2)])
   4.132 -                            val newenv = getnewenv unif_env
   4.133 -                            val envlist = Envir.alist_of newenv
   4.134 -                            
   4.135 -                            val (t1,t2)::_ = mksubstlist envlist []
   4.136 -                          in 
   4.137 -                            if (is_Var t1)
   4.138 -                            then
   4.139 -                                let 
   4.140 -                                   val str1 = lit_string_with_nums t1;
   4.141 -                                   val str2 = lit_string_with_nums t2;
   4.142 -                                   val facthm = read_instantiate [(str1,str2)] th;
   4.143 -                                   val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
   4.144 -                                   val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
   4.145 -                                   val thmvars = thm_vars res'
   4.146 -                                in 
   4.147 -                                       (res',((Factor (clause,  lit1, lit2)),clause_strs,thmvars))
   4.148 -                                end
   4.149 -                            else
   4.150 -                                let
   4.151 -                                   val str2 = lit_string_with_nums t1;
   4.152 -                                   val str1 = lit_string_with_nums t2;
   4.153 -                                   val facthm = read_instantiate [(str1,str2)] th;
   4.154 -                                   val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
   4.155 -                                   val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars)
   4.156 -                                  val thmvars = thm_vars res'
   4.157 -                                in 
   4.158 -                                       (res', ((Factor (clause,  lit1, lit2)),clause_strs, thmvars))         
   4.159 -                                end
   4.160 -                         end
   4.161 -                         handle Option => reconstruction_failed "follow_factor"
   4.162 +fun follow_factor clause lit1 lit2 allvars thml clause_strs = 
   4.163 +    let 
   4.164 +      val th =  valOf (assoc (thml,clause))
   4.165 +      val prems = prems_of th
   4.166 +      val sign = sign_of_thm th
   4.167 +      val fac1 = ReconOrderClauses.get_nth (lit1+1) prems
   4.168 +      val fac2 = ReconOrderClauses.get_nth (lit2+1) prems
   4.169 +      val unif_env = Unify.unifiers (sign,Envir.empty 0, [(fac1, fac2)])
   4.170 +      val newenv = getnewenv unif_env
   4.171 +      val envlist = Envir.alist_of newenv
   4.172 +      
   4.173 +      val (t1,t2)::_ = mksubstlist envlist []
   4.174 +    in 
   4.175 +      if (is_Var t1)
   4.176 +      then
   4.177 +	  let 
   4.178 +	     val str1 = lit_string_with_nums t1;
   4.179 +	     val str2 = lit_string_with_nums t2;
   4.180 +	     val facthm = read_instantiate [(str1,str2)] th;
   4.181 +	     val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
   4.182 +	     val (res', numlist, symlist, nsymlist) = 
   4.183 +	         ReconOrderClauses.rearrange_clause res clause_strs allvars
   4.184 +	     val thmvars = thm_vars res'
   4.185 +	  in 
   4.186 +		 (res',((Factor (clause,  lit1, lit2)),clause_strs,thmvars))
   4.187 +	  end
   4.188 +      else
   4.189 +	  let
   4.190 +	     val str2 = lit_string_with_nums t1;
   4.191 +	     val str1 = lit_string_with_nums t2;
   4.192 +	     val facthm = read_instantiate [(str1,str2)] th;
   4.193 +	     val res = hd (Seq.list_of(delete_assump_tac  facthm (lit1 + 1)))
   4.194 +	     val (res', numlist, symlist, nsymlist) = 
   4.195 +	         ReconOrderClauses.rearrange_clause res clause_strs allvars
   4.196 +	     val thmvars = thm_vars res'
   4.197 +	  in 
   4.198 +		 (res', ((Factor (clause,  lit1, lit2)),clause_strs, thmvars))         
   4.199 +	  end
   4.200 +   end
   4.201 +   handle Option => reconstruction_failed "follow_factor"
   4.202  
   4.203  
   4.204  
   4.205 @@ -216,28 +220,29 @@
   4.206  val rev_ssubst = rotate_prems 1 ssubst;
   4.207  
   4.208  
   4.209 -fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= 
   4.210 -                          let 
   4.211 -                            val th1 =  valOf (assoc (thml,clause1))
   4.212 -                            val th2 =  valOf (assoc (thml,clause2)) 
   4.213 -                            val eq_lit_th = select_literal (lit1+1) th1
   4.214 -                            val mod_lit_th = select_literal (lit2+1) th2
   4.215 -                            val eqsubst = eq_lit_th RSN (2,rev_subst)
   4.216 -                            val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
   4.217 -			    val newth' =negate_head newth 
   4.218 -                            val (res, numlist, symlist, nsymlist)  = (rearrange_clause newth' clause_strs allvars 
   4.219 -                                handle Not_in_list => let 
   4.220 -                                                  val mod_lit_th' = mod_lit_th RS not_sym
   4.221 -                                                   val newth = Seq.hd (biresolution false [(false, mod_lit_th')] 1 eqsubst)
   4.222 -			                           val newth' =negate_head newth 
   4.223 -                                               in 
   4.224 -                                                  (rearrange_clause newth' clause_strs allvars)
   4.225 -                                               end)
   4.226 -                            val thmvars = thm_vars res
   4.227 -                         in 
   4.228 -                           (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
   4.229 -                         end
   4.230 -			 handle Option => reconstruction_failed "follow_standard_para"
   4.231 +fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs = 
   4.232 +    let 
   4.233 +      val th1 =  valOf (assoc (thml,clause1))
   4.234 +      val th2 =  valOf (assoc (thml,clause2)) 
   4.235 +      val eq_lit_th = select_literal (lit1+1) th1
   4.236 +      val mod_lit_th = select_literal (lit2+1) th2
   4.237 +      val eqsubst = eq_lit_th RSN (2,rev_subst)
   4.238 +      val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
   4.239 +      val newth' =negate_head newth 
   4.240 +      val (res, numlist, symlist, nsymlist)  = 
   4.241 +          (ReconOrderClauses.rearrange_clause newth' clause_strs allvars 
   4.242 +	   handle Not_in_list => 
   4.243 +	       let val mod_lit_th' = mod_lit_th RS not_sym
   4.244 +		   val newth = Seq.hd (biresolution false [(false, mod_lit_th')] 1 eqsubst)
   4.245 +		   val newth' =negate_head newth 
   4.246 +		in 
   4.247 +		   ReconOrderClauses.rearrange_clause newth' clause_strs allvars
   4.248 +		end)
   4.249 +      val thmvars = thm_vars res
   4.250 +   in 
   4.251 +     (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars))
   4.252 +   end
   4.253 +   handle Option => reconstruction_failed "follow_standard_para"
   4.254  
   4.255  (*              
   4.256  fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= 
   4.257 @@ -293,26 +298,24 @@
   4.258  (* extra conditions from the equality turn up as 2nd to last literals of result.  Need to delete them *)
   4.259  (* changed negate_nead to negate_head here too*)
   4.260                      (* clause1, lit1 is thing to rewrite with *)
   4.261 -fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs= 
   4.262 -
   4.263 -                          let val th1 =  valOf (assoc (thml,clause1))
   4.264 -                              val th2 = valOf (assoc (thml,clause2))
   4.265 -                              val eq_lit_th = select_literal (lit1+1) th1
   4.266 -                              val mod_lit_th = select_literal (lit2+1) th2
   4.267 -                              val eqsubst = eq_lit_th RSN (2,rev_subst)
   4.268 -                              val eq_lit_prem_num = length (prems_of eq_lit_th)
   4.269 -                              val sign = Sign.merge (sign_of_thm th1, sign_of_thm th2)
   4.270 -                              val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 
   4.271 -eqsubst)
   4.272 -                         
   4.273 -                              val newthm = negate_head newth
   4.274 -                              val newthm' = delete_assumps eq_lit_prem_num newthm
   4.275 -                              val (res, numlist, symlist, nsymlist) =(rearrange_clause newthm clause_strs allvars)
   4.276 -                              val thmvars = thm_vars res
   4.277 -                           in
   4.278 -                               (res, ((Rewrite ((clause1, lit1),  (clause2, lit2))),clause_strs,thmvars))
   4.279 -                           end
   4.280 -			   handle Option => reconstruction_failed "follow_rewrite"
   4.281 +fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs = 
   4.282 +      let val th1 =  valOf (assoc (thml,clause1))
   4.283 +	  val th2 = valOf (assoc (thml,clause2))
   4.284 +	  val eq_lit_th = select_literal (lit1+1) th1
   4.285 +	  val mod_lit_th = select_literal (lit2+1) th2
   4.286 +	  val eqsubst = eq_lit_th RSN (2,rev_subst)
   4.287 +	  val eq_lit_prem_num = length (prems_of eq_lit_th)
   4.288 +	  val sign = Sign.merge (sign_of_thm th1, sign_of_thm th2)
   4.289 +	  val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
   4.290 +     	  val newthm = negate_head newth
   4.291 +	  val newthm' = delete_assumps eq_lit_prem_num newthm
   4.292 +	  val (res, numlist, symlist, nsymlist) =
   4.293 +	      ReconOrderClauses.rearrange_clause newthm clause_strs allvars
   4.294 +	  val thmvars = thm_vars res
   4.295 +       in
   4.296 +	   (res, ((Rewrite ((clause1, lit1),  (clause2, lit2))),clause_strs,thmvars))
   4.297 +       end
   4.298 +       handle Option => reconstruction_failed "follow_rewrite"
   4.299  
   4.300  
   4.301  
   4.302 @@ -321,17 +324,18 @@
   4.303  (*****************************************)
   4.304  
   4.305  
   4.306 -fun follow_obvious  (clause1, lit1)  allvars thml clause_strs= 
   4.307 -                           let val th1 =  valOf (assoc (thml,clause1))
   4.308 -                               val prems1 = prems_of th1
   4.309 -                               val newthm = refl RSN ((lit1+ 1), th1)
   4.310 -                                               handle THM _ =>  hd (Seq.list_of(delete_assump_tac  th1 (lit1 + 1)))
   4.311 -                               val (res, numlist, symlist, nsymlist) =(rearrange_clause newthm clause_strs allvars)
   4.312 -                               val thmvars = thm_vars res
   4.313 -                           in 
   4.314 -                               (res, ((Obvious (clause1, lit1)),clause_strs,thmvars))
   4.315 -                           end
   4.316 -  	 		   handle Option => reconstruction_failed "follow_obvious"
   4.317 +fun follow_obvious  (clause1, lit1)  allvars thml clause_strs = 
   4.318 +    let val th1 =  valOf (assoc (thml,clause1))
   4.319 +	val prems1 = prems_of th1
   4.320 +	val newthm = refl RSN ((lit1+ 1), th1)
   4.321 +		     handle THM _ =>  hd (Seq.list_of(delete_assump_tac  th1 (lit1 + 1)))
   4.322 +	val (res, numlist, symlist, nsymlist) =
   4.323 +	    ReconOrderClauses.rearrange_clause newthm clause_strs allvars
   4.324 +	val thmvars = thm_vars res
   4.325 +    in 
   4.326 +	(res, ((Obvious (clause1, lit1)),clause_strs,thmvars))
   4.327 +    end
   4.328 +    handle Option => reconstruction_failed "follow_obvious"
   4.329  
   4.330  (**************************************************************************************)
   4.331  (* reconstruct a single line of the res. proof - depending on what sort of proof step it was*)
   4.332 @@ -436,28 +440,29 @@
   4.333  
   4.334  *)
   4.335  
   4.336 -fun replace_clause_strs [] recons newrecons= (newrecons)
   4.337 -|   replace_clause_strs ((thmnum, thm)::thml)  ((clausenum,(step,clause_strs,thmvars))::recons) newrecons = 
   4.338 -                           let val new_clause_strs = get_meta_lits_bracket thm
   4.339 -                           in
   4.340 -                               replace_clause_strs thml recons ((clausenum,(step,new_clause_strs,thmvars))::newrecons)
   4.341 -                           end
   4.342 +fun replace_clause_strs [] recons newrecons = (newrecons)
   4.343 +|   replace_clause_strs ((thmnum, thm)::thml)    
   4.344 +                  ((clausenum,(step,clause_strs,thmvars))::recons) newrecons = 
   4.345 +    let val new_clause_strs = ReconOrderClauses.get_meta_lits_bracket thm
   4.346 +    in
   4.347 +	replace_clause_strs thml recons  
   4.348 +	    ((clausenum,(step,new_clause_strs,thmvars))::newrecons)
   4.349 +    end
   4.350  
   4.351  
   4.352  fun follow clauses [] allvars thml recons = 
   4.353 -                             let 
   4.354 -                                 val new_recons = replace_clause_strs thml recons []
   4.355 -                             in
   4.356 -                                  ((snd( hd thml)), new_recons)
   4.357 -                             end
   4.358 -
   4.359 - |  follow clauses (h::t) allvars thml recons 
   4.360 -        = let
   4.361 -            val (thml', recons') = follow_line clauses allvars  thml h recons
   4.362 -            val  (thm, recons_list) = follow clauses t  allvars thml' recons'     
   4.363 -          in
   4.364 -             (thm,recons_list)
   4.365 -          end
   4.366 +      let 
   4.367 +	  val new_recons = replace_clause_strs thml recons []
   4.368 +      in
   4.369 +	   (#2(hd thml), new_recons)
   4.370 +      end
   4.371 + | follow clauses (h::t) allvars thml recons =
   4.372 +      let
   4.373 +	val (thml', recons') = follow_line clauses allvars  thml h recons
   4.374 +	val  (thm, recons_list) = follow clauses t  allvars thml' recons'     
   4.375 +      in
   4.376 +	 (thm,recons_list)
   4.377 +      end
   4.378  
   4.379  
   4.380  
   4.381 @@ -481,4 +486,5 @@
   4.382  
   4.383  
   4.384  fun remove_tinfo [] = []
   4.385 -|   remove_tinfo ( (clausenum, step, T_info, newstrs)::xs) = (clausenum, step , newstrs)::(remove_tinfo xs)
   4.386 +  | remove_tinfo ( (clausenum, step, T_info, newstrs)::xs) =
   4.387 +      (clausenum, step , newstrs)::(remove_tinfo xs)
     5.1 --- a/src/HOL/Tools/ATP/res_clasimpset.ML	Tue May 24 07:43:38 2005 +0200
     5.2 +++ b/src/HOL/Tools/ATP/res_clasimpset.ML	Tue May 24 10:23:24 2005 +0200
     5.3 @@ -12,18 +12,10 @@
     5.4  
     5.5  structure ResClasimp : RES_CLASIMP =
     5.6  struct
     5.7 -fun has_name th = not((Thm.name_of_thm th )= "")
     5.8 -fun has_name_pair (a,b) = not_equal a "";
     5.9 -
    5.10 -fun stick []  = []
    5.11 -|   stick (x::xs)  = x@(stick xs )
    5.12  
    5.13 -fun filterlist p [] = []
    5.14 -|   filterlist p (x::xs) = if p x 
    5.15 -                           then 
    5.16 -                               (x::(filterlist p xs))
    5.17 -                           else
    5.18 -                               filterlist p xs
    5.19 +fun has_name th = ((Thm.name_of_thm th)  <>  "")
    5.20 +
    5.21 +fun has_name_pair (a,b) = (a <> "");
    5.22  
    5.23  
    5.24  (* changed, now it also finds out the name of the theorem. *)
    5.25 @@ -37,73 +29,64 @@
    5.26    | concat_with_stop [x] =  x
    5.27    | concat_with_stop (x::xs) = x^ "." ^ concat_with_stop xs;
    5.28  
    5.29 -fun remove_symb str = if String.isPrefix  "List.op @." str
    5.30 -                      then 
    5.31 -                          ((String.substring(str,0,5))^(String.extract (str, 10, NONE)))
    5.32 -                      else
    5.33 -                          str
    5.34 -
    5.35 -fun remove_spaces str = let val strlist = String.tokens Char.isSpace str
    5.36 -                            val spaceless = concat strlist
    5.37 -                            val strlist' = String.tokens Char.isPunct spaceless
    5.38 -                        in
    5.39 -                            concat_with_stop strlist'
    5.40 -                        end
    5.41 +fun remove_symb str = 
    5.42 +    if String.isPrefix  "List.op @." str
    5.43 +    then  ((String.substring(str,0,5)) ^ (String.extract (str, 10, NONE)))
    5.44 +    else str;
    5.45  
    5.46 -fun remove_symb_pair (str, thm) = let val newstr = remove_symb str
    5.47 -                                  in
    5.48 -                                    (newstr, thm)
    5.49 -                                  end
    5.50 -
    5.51 +fun remove_spaces str = 
    5.52 +    let val strlist = String.tokens Char.isSpace str
    5.53 +	val spaceless = concat strlist
    5.54 +	val strlist' = String.tokens Char.isPunct spaceless
    5.55 +    in
    5.56 +	concat_with_stop strlist'
    5.57 +    end
    5.58  
    5.59 -fun remove_spaces_pair (str, thm) = let val newstr = remove_spaces str
    5.60 -                                  in
    5.61 -                                    (newstr, thm)
    5.62 -                                  end
    5.63 +fun remove_symb_pair (str, thm) = (remove_symb str, thm);
    5.64  
    5.65 -
    5.66 +fun remove_spaces_pair (str, thm) = (remove_spaces str, thm);
    5.67  
    5.68  
    5.69  (*Insert th into the result provided the name is not "".*)
    5.70  fun add_nonempty ((name,th), ths) = if name="" then ths else th::ths;
    5.71  
    5.72  
    5.73 -fun write_out_clasimp filename = let
    5.74 -					val claset_rules = ResAxioms.claset_rules_of_thy (the_context());
    5.75 -					val named_claset = filterlist has_name_pair claset_rules;
    5.76 -					val claset_names = map remove_spaces_pair (named_claset)
    5.77 -					val claset_cls_thms = #1( ResAxioms.clausify_rules_pairs named_claset []);
    5.78 -
    5.79 +fun write_out_clasimp filename = 
    5.80 +    let val claset_rules = ResAxioms.claset_rules_of_thy (the_context());
    5.81 +	val named_claset = List.filter has_name_pair claset_rules;
    5.82 +	val claset_names = map remove_spaces_pair (named_claset)
    5.83 +	val claset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_claset []);
    5.84  
    5.85 -					val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context());
    5.86 -					val named_simpset = map remove_spaces_pair (filterlist has_name_pair simpset_rules);
    5.87 -					val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
    5.88 +	val simpset_rules = ResAxioms.simpset_rules_of_thy (the_context());
    5.89 +	val named_simpset = 
    5.90 +	      map remove_spaces_pair (List.filter has_name_pair simpset_rules)
    5.91 +	val simpset_cls_thms = #1 (ResAxioms.clausify_rules_pairs named_simpset []);
    5.92  
    5.93 -					val cls_thms = (claset_cls_thms@simpset_cls_thms);
    5.94 -					val cls_thms_list = stick cls_thms;
    5.95 +	val cls_thms = (claset_cls_thms@simpset_cls_thms);
    5.96 +	val cls_thms_list = List.concat cls_thms;
    5.97  
    5.98 -                                        (*********************************************************)
    5.99 -                                  	(* create array and put clausename, number pairs into it *)
   5.100 -                                   	(*********************************************************)
   5.101 -					val num_of_clauses =  0;
   5.102 -                                     	val clause_arr = Array.fromList cls_thms_list;
   5.103 -              
   5.104 -                                   	val  num_of_clauses= (List.length cls_thms_list);
   5.105 +	(*********************************************************)
   5.106 +	(* create array and put clausename, number pairs into it *)
   5.107 +	(*********************************************************)
   5.108 +	val num_of_clauses =  0;
   5.109 +	val clause_arr = Array.fromList cls_thms_list;
   5.110 +
   5.111 +	val num_of_clauses = List.length cls_thms_list;
   5.112  
   5.113 -                                        (*************************************************)
   5.114 -					(* Write out clauses as tptp strings to filename *)
   5.115 - 					(*************************************************)
   5.116 -                                        val clauses = map #1(cls_thms_list);
   5.117 -          				val cls_tptp_strs = map ResClause.tptp_clause clauses;
   5.118 -                                        (* list of lists of tptp string clauses *)
   5.119 -                                        val stick_clasrls =   stick cls_tptp_strs;
   5.120 -    					val out = TextIO.openOut filename;
   5.121 -                                    	val _=   ResLib.writeln_strs out stick_clasrls;
   5.122 -                                    	val _= TextIO.flushOut out;
   5.123 -					val _= TextIO.closeOut out
   5.124 -                     		  in
   5.125 -					(clause_arr, num_of_clauses)
   5.126 -				  end;
   5.127 +	(*************************************************)
   5.128 +	(* Write out clauses as tptp strings to filename *)
   5.129 +	(*************************************************)
   5.130 +	val clauses = map #1(cls_thms_list);
   5.131 +	val cls_tptp_strs = map ResClause.tptp_clause clauses;
   5.132 +	(* list of lists of tptp string clauses *)
   5.133 +	val stick_clasrls =   List.concat cls_tptp_strs;
   5.134 +	val out = TextIO.openOut filename;
   5.135 +	val _=   ResLib.writeln_strs out stick_clasrls;
   5.136 +	val _= TextIO.flushOut out;
   5.137 +	val _= TextIO.closeOut out
   5.138 +  in
   5.139 +	(clause_arr, num_of_clauses)
   5.140 +  end;
   5.141  
   5.142  
   5.143  end;
     6.1 --- a/src/HOL/Tools/ATP/watcher.ML	Tue May 24 07:43:38 2005 +0200
     6.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Tue May 24 10:23:24 2005 +0200
     6.3 @@ -164,44 +164,45 @@
     6.4  fun callResProvers (toWatcherStr,  []) = (sendOutput (toWatcherStr, "End of calls\n"); 
     6.5                                       TextIO.flushOut toWatcherStr)
     6.6  |   callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile,probfile)::args) =
     6.7 -                                                     let val dfg_dir = File.tmp_path (Path.basic "dfg"); 
     6.8 -                                                        (*** need to check here if the directory exists and, if not, create it***)
     6.9 -                                                         val  outfile = TextIO.openAppend(File.sysify_path
    6.10 -                                                                               (File.tmp_path (Path.basic"thmstring_in_watcher")));                                                                         val _ = TextIO.output (outfile, 
    6.11 -                                                                       (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
    6.12 -                                                         val _ =  TextIO.closeOut outfile
    6.13 -                                                        (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
    6.14 -							val probID = last(explode probfile)
    6.15 -                                                         val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
    6.16 -                                                         (*** only include problem and clasimp for the moment, not sure how to refer to ***)
    6.17 -                                                         (*** hyps/local axioms just now                                                ***)
    6.18 -                                                         val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile,  ">", (File.sysify_path wholefile)])
    6.19 -                                                         val dfg_create =if File.exists dfg_dir 
    6.20 -                                                                         then
    6.21 -                                                                             ((warning("dfg dir exists"));())
    6.22 -                                                                         else
    6.23 -                                                                               File.mkdir dfg_dir; 
    6.24 -                                                         
    6.25 -                                                         val dfg_path = File.sysify_path dfg_dir;
    6.26 -                                                         val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X",   ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path])
    6.27 -                                                       (*val _ = Posix.Process.wait ()*)
    6.28 -                                                       (*val _ =Unix.reap exec_tptp2x*)
    6.29 -                                                         val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
    6.30 -                                       
    6.31 -                                                      in   
    6.32 -                                                         goals_being_watched := (!goals_being_watched) + 1;
    6.33 -                                                         Posix.Process.sleep(Time.fromSeconds 1); 
    6.34 -                     					(warning ("probfile is: "^probfile));
    6.35 -                                                         (warning("dfg file is: "^newfile));
    6.36 -                                                         (warning ("wholefile is: "^(File.sysify_path wholefile)));
    6.37 -                                                        sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n"));
    6.38 -(*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*)
    6.39 -                                                         TextIO.flushOut toWatcherStr;
    6.40 -                                                         Unix.reap exec_tptp2x; 
    6.41 -                                                         
    6.42 -                                                         callResProvers (toWatcherStr,args)
    6.43 -                                           
    6.44 -                                                     end
    6.45 +      let val dfg_dir = File.tmp_path (Path.basic "dfg"); 
    6.46 +	 (*** need to check here if the directory exists and, if not, create it***)
    6.47 +	  val  outfile = TextIO.openAppend(File.sysify_path
    6.48 +				(File.tmp_path (Path.basic"thmstring_in_watcher")));                                                                         
    6.49 +	  val _ = TextIO.output (outfile, 
    6.50 +			(thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
    6.51 +	  val _ =  TextIO.closeOut outfile
    6.52 +	 (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
    6.53 +	 val probID = ReconOrderClauses.last(explode probfile)
    6.54 +	  val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
    6.55 +	  (*** only include problem and clasimp for the moment, not sure how to refer to ***)
    6.56 +	  (*** hyps/local axioms just now                                                ***)
    6.57 +	  val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile,  ">", (File.sysify_path wholefile)])
    6.58 +	  val dfg_create =if File.exists dfg_dir 
    6.59 +			  then
    6.60 +			      ((warning("dfg dir exists"));())
    6.61 +			  else
    6.62 +				File.mkdir dfg_dir; 
    6.63 +	  
    6.64 +	  val dfg_path = File.sysify_path dfg_dir;
    6.65 +	  val exec_tptp2x = Unix.execute("/usr/groups/theory/tptp/TPTP-v3.0.1/TPTP2X/tptp2X",   ["-fdfg ",(File.sysify_path wholefile)," -d ",dfg_path])
    6.66 +	(*val _ = Posix.Process.wait ()*)
    6.67 +	(*val _ =Unix.reap exec_tptp2x*)
    6.68 +	  val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
    6.69 + 
    6.70 +       in   
    6.71 +	  goals_being_watched := (!goals_being_watched) + 1;
    6.72 +	  Posix.Process.sleep(Time.fromSeconds 1); 
    6.73 +	 (warning ("probfile is: "^probfile));
    6.74 +	  (warning("dfg file is: "^newfile));
    6.75 +	  (warning ("wholefile is: "^(File.sysify_path wholefile)));
    6.76 +	 sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^newfile^"\n"));
    6.77 + (*sendOutput (toWatcherStr, (prover^"*"^thmstring^"*"^goalstring^"*"^proverCmd^"*"^settings^"*"^"/homes/clq20/IsabelleCVS/isabelle/HOL/Tools/ATP/dfg/mini_p1.dfg"^"\n"));*)
    6.78 +	  TextIO.flushOut toWatcherStr;
    6.79 +	  Unix.reap exec_tptp2x; 
    6.80 +	  
    6.81 +	  callResProvers (toWatcherStr,args)
    6.82 + 
    6.83 +      end
    6.84  (*
    6.85  fun callResProversStr (toWatcherStr,  []) =  "End of calls\n" 
    6.86                                       
    6.87 @@ -327,374 +328,375 @@
    6.88  
    6.89  
    6.90  
    6.91 -fun setupWatcher (thm,clause_arr, num_of_clauses) = let
    6.92 -          (** pipes for communication between parent and watcher **)
    6.93 -          val p1 = Posix.IO.pipe ()
    6.94 -          val p2 = Posix.IO.pipe ()
    6.95 -	  fun closep () = (
    6.96 -                Posix.IO.close (#outfd p1); 
    6.97 -                Posix.IO.close (#infd p1);
    6.98 -                Posix.IO.close (#outfd p2); 
    6.99 -                Posix.IO.close (#infd p2)
   6.100 -              )
   6.101 -          (***********************************************************)
   6.102 -          (****** fork a watcher process and get it set up and going *)
   6.103 -          (***********************************************************)
   6.104 -          fun startWatcher (procList) =
   6.105 -                   (case  Posix.Process.fork() (***************************************)
   6.106 -		 of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
   6.107 -                                               (***************************************)
   6.108 - 
   6.109 -                                                 (*************************)
   6.110 -                  | NONE => let                  (* child - i.e. watcher  *)
   6.111 -		      val oldchildin = #infd p1  (*************************)
   6.112 -		      val fromParent = Posix.FileSys.wordToFD 0w0
   6.113 -		      val oldchildout = #outfd p2
   6.114 -		      val toParent = Posix.FileSys.wordToFD 0w1
   6.115 -                      val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   6.116 -                      val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   6.117 -                      val toParentStr = openOutFD ("_exec_out_parent", toParent)
   6.118 -                      val sign = sign_of_thm thm
   6.119 -                      val prems = prems_of thm
   6.120 -                      val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   6.121 -                      val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
   6.122 -                     (* tracing *)
   6.123 -		    (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
   6.124 -                      val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)
   6.125 -                      val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
   6.126 -                      val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))         
   6.127 -                      val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))         
   6.128 -                      val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )       
   6.129 -                               *)
   6.130 -                      (*val goalstr = string_of_thm (the_goal)
   6.131 -                       val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher")));  
   6.132 -                      val _ = TextIO.output (outfile,goalstr )
   6.133 -                      val _ =  TextIO.closeOut outfile*)
   6.134 -                      fun killChildren [] = ()
   6.135 -                   |      killChildren  (child_handle::children) = (killChild child_handle; killChildren children)
   6.136 +fun setupWatcher (thm,clause_arr, num_of_clauses) = 
   6.137 +  let
   6.138 +    (** pipes for communication between parent and watcher **)
   6.139 +    val p1 = Posix.IO.pipe ()
   6.140 +    val p2 = Posix.IO.pipe ()
   6.141 +    fun closep () = (
   6.142 +	  Posix.IO.close (#outfd p1); 
   6.143 +	  Posix.IO.close (#infd p1);
   6.144 +	  Posix.IO.close (#outfd p2); 
   6.145 +	  Posix.IO.close (#infd p2)
   6.146 +	)
   6.147 +    (***********************************************************)
   6.148 +    (****** fork a watcher process and get it set up and going *)
   6.149 +    (***********************************************************)
   6.150 +    fun startWatcher (procList) =
   6.151 +	     (case  Posix.Process.fork() (***************************************)
   6.152 +	   of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
   6.153 +					 (***************************************)
   6.154 +
   6.155 +					   (*************************)
   6.156 +	    | NONE => let                  (* child - i.e. watcher  *)
   6.157 +		val oldchildin = #infd p1  (*************************)
   6.158 +		val fromParent = Posix.FileSys.wordToFD 0w0
   6.159 +		val oldchildout = #outfd p2
   6.160 +		val toParent = Posix.FileSys.wordToFD 0w1
   6.161 +		val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   6.162 +		val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   6.163 +		val toParentStr = openOutFD ("_exec_out_parent", toParent)
   6.164 +		val sign = sign_of_thm thm
   6.165 +		val prems = prems_of thm
   6.166 +		val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   6.167 +		val _ = (warning ("subgoals forked to startWatcher: "^prems_string));
   6.168 +	       (* tracing *)
   6.169 +	      (*val tenth_ax = fst( Array.sub(clause_arr, 1))  
   6.170 +		val tenth_ax_thms = memo_find_clause (tenth_ax, clause_tab)
   6.171 +		val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms)
   6.172 +		val _ = (warning ("tenth axiom in array in watcher is: "^tenth_ax))         
   6.173 +		val _ = (warning ("tenth axiom in table in watcher is: "^clause_str))         
   6.174 +		val _ = (warning ("num_of_clauses in watcher is: "^(string_of_int (num_of_clauses))) )       
   6.175 +			 *)
   6.176 +		(*val goalstr = string_of_thm (the_goal)
   6.177 +		 val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "goal_in_watcher")));  
   6.178 +		val _ = TextIO.output (outfile,goalstr )
   6.179 +		val _ =  TextIO.closeOut outfile*)
   6.180 +		fun killChildren [] = ()
   6.181 +	     |      killChildren  (child_handle::children) = (killChild child_handle; killChildren children)
   6.182  
   6.183 -                     
   6.184 -           
   6.185 -                    (*************************************************************)
   6.186 -                    (* take an instream and poll its underlying reader for input *)
   6.187 -                    (*************************************************************)
   6.188 +	       
   6.189 +     
   6.190 +	      (*************************************************************)
   6.191 +	      (* take an instream and poll its underlying reader for input *)
   6.192 +	      (*************************************************************)
   6.193  
   6.194 -                    fun pollParentInput () = 
   6.195 -                           
   6.196 -                               let val pd = OS.IO.pollDesc (fromParentIOD)
   6.197 -                               in 
   6.198 -                               if (isSome pd ) then 
   6.199 -                                   let val pd' = OS.IO.pollIn (valOf pd)
   6.200 -                                       val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
   6.201 -                                   in
   6.202 -                                      if null pdl 
   6.203 -                                      then
   6.204 -                                         NONE
   6.205 -                                      else if (OS.IO.isIn (hd pdl)) 
   6.206 -                                           then
   6.207 -                                              (SOME ( getCmds (toParentStr, fromParentStr, [])))
   6.208 -                                           else
   6.209 -                                               NONE
   6.210 -                                   end
   6.211 -                                 else
   6.212 -                                     NONE
   6.213 -                                 end
   6.214 -                            
   6.215 -                   
   6.216 +	      fun pollParentInput () = 
   6.217 +		     
   6.218 +			 let val pd = OS.IO.pollDesc (fromParentIOD)
   6.219 +			 in 
   6.220 +			 if (isSome pd ) then 
   6.221 +			     let val pd' = OS.IO.pollIn (valOf pd)
   6.222 +				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
   6.223 +			     in
   6.224 +				if null pdl 
   6.225 +				then
   6.226 +				   NONE
   6.227 +				else if (OS.IO.isIn (hd pdl)) 
   6.228 +				     then
   6.229 +					(SOME ( getCmds (toParentStr, fromParentStr, [])))
   6.230 +				     else
   6.231 +					 NONE
   6.232 +			     end
   6.233 +			   else
   6.234 +			       NONE
   6.235 +			   end
   6.236 +		      
   6.237 +	     
   6.238  
   6.239 -                     fun pollChildInput (fromStr) = 
   6.240 -                           let val iod = getInIoDesc fromStr
   6.241 -                           in 
   6.242 -                           if isSome iod 
   6.243 -                           then 
   6.244 -                               let val pd = OS.IO.pollDesc (valOf iod)
   6.245 -                               in 
   6.246 -                               if (isSome pd ) then 
   6.247 -                                   let val pd' = OS.IO.pollIn (valOf pd)
   6.248 -                                       val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
   6.249 -                                   in
   6.250 -                                      if null pdl 
   6.251 -                                      then
   6.252 -                                         NONE
   6.253 -                                      else if (OS.IO.isIn (hd pdl)) 
   6.254 -                                           then
   6.255 -                                               SOME (getCmd (TextIO.inputLine fromStr))
   6.256 -                                           else
   6.257 -                                               NONE
   6.258 -                                   end
   6.259 -                                 else
   6.260 -                                     NONE
   6.261 -                                 end
   6.262 -                             else 
   6.263 -                                 NONE
   6.264 -                            end
   6.265 +	       fun pollChildInput (fromStr) = 
   6.266 +		     let val iod = getInIoDesc fromStr
   6.267 +		     in 
   6.268 +		     if isSome iod 
   6.269 +		     then 
   6.270 +			 let val pd = OS.IO.pollDesc (valOf iod)
   6.271 +			 in 
   6.272 +			 if (isSome pd ) then 
   6.273 +			     let val pd' = OS.IO.pollIn (valOf pd)
   6.274 +				 val pdl = OS.IO.poll ([pd'], SOME (Time.fromMilliseconds 100)) 
   6.275 +			     in
   6.276 +				if null pdl 
   6.277 +				then
   6.278 +				   NONE
   6.279 +				else if (OS.IO.isIn (hd pdl)) 
   6.280 +				     then
   6.281 +					 SOME (getCmd (TextIO.inputLine fromStr))
   6.282 +				     else
   6.283 +					 NONE
   6.284 +			     end
   6.285 +			   else
   6.286 +			       NONE
   6.287 +			   end
   6.288 +		       else 
   6.289 +			   NONE
   6.290 +		      end
   6.291  
   6.292  
   6.293 -                   (****************************************************************************)
   6.294 -                   (* Check all vampire processes currently running for output                 *)
   6.295 -                   (****************************************************************************) 
   6.296 -                                                              (*********************************)
   6.297 -                    fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
   6.298 -                                                              (*********************************)
   6.299 -                    |   checkChildren ((childProc::otherChildren), toParentStr) = 
   6.300 -                                            let val (childInput,childOutput) =  cmdstreamsOf childProc
   6.301 -                                                val child_handle= cmdchildHandle childProc
   6.302 -                                                (* childCmd is the .dfg file that the problem is in *)
   6.303 -                                                val childCmd = fst(snd (cmdchildInfo childProc))
   6.304 -                                                (* now get the number of the subgoal from the filename *)
   6.305 -                                                val sg_num = int_of_string(get_nth 5 (rev(explode childCmd)))
   6.306 -                                                val childIncoming = pollChildInput childInput
   6.307 -                                                val parentID = Posix.ProcEnv.getppid()
   6.308 -                                                val prover = cmdProver childProc
   6.309 -                                                val thmstring = cmdThm childProc
   6.310 -                                                val sign = sign_of_thm thm
   6.311 -                                                val prems = prems_of thm
   6.312 -                                                val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   6.313 -                                                val _ = (warning ("subgoals forked to checkChildren: "^prems_string));
   6.314 -                                                val goalstring = cmdGoal childProc
   6.315 -                                                                                                       
   6.316 -                                                val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_comms")));  
   6.317 -                                                val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
   6.318 -                                                val _ =  TextIO.closeOut outfile
   6.319 -                                            in 
   6.320 -                                              if (isSome childIncoming) 
   6.321 -                                              then 
   6.322 -                                                  (* check here for prover label on child*)
   6.323 -                                                   
   6.324 -                                                  let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));  
   6.325 -                                                val _ = TextIO.output (outfile,(("subgoals forked to checkChildren: "^prems_string)^prover^thmstring^goalstring^childCmd) )
   6.326 -                                                val _ =  TextIO.closeOut outfile
   6.327 -                                              val childDone = (case prover of
   6.328 -                                    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
   6.329 -                                                   in
   6.330 -                                                    if childDone      (**********************************************)
   6.331 -                                                    then              (* child has found a proof and transferred it *)
   6.332 -                                                                      (**********************************************)
   6.333 +	     (****************************************************************************)
   6.334 +	     (* Check all vampire processes currently running for output                 *)
   6.335 +	     (****************************************************************************) 
   6.336 +							(*********************************)
   6.337 +	      fun checkChildren ([], toParentStr) = []  (*** no children to check ********)
   6.338 +							(*********************************)
   6.339 +	      |   checkChildren ((childProc::otherChildren), toParentStr) = 
   6.340 +		    let val (childInput,childOutput) =  cmdstreamsOf childProc
   6.341 +			val child_handle= cmdchildHandle childProc
   6.342 +			(* childCmd is the .dfg file that the problem is in *)
   6.343 +			val childCmd = fst(snd (cmdchildInfo childProc))
   6.344 +			(* now get the number of the subgoal from the filename *)
   6.345 +			val sg_num = int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))
   6.346 +			val childIncoming = pollChildInput childInput
   6.347 +			val parentID = Posix.ProcEnv.getppid()
   6.348 +			val prover = cmdProver childProc
   6.349 +			val thmstring = cmdThm childProc
   6.350 +			val sign = sign_of_thm thm
   6.351 +			val prems = prems_of thm
   6.352 +			val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   6.353 +			val _ = (warning ("subgoals forked to checkChildren: "^prems_string));
   6.354 +			val goalstring = cmdGoal childProc
   6.355 +									       
   6.356 +			val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_comms")));  
   6.357 +			val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
   6.358 +			val _ =  TextIO.closeOut outfile
   6.359 +		    in 
   6.360 +		      if (isSome childIncoming) 
   6.361 +		      then 
   6.362 +			  (* check here for prover label on child*)
   6.363 +			   
   6.364 +			  let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));  
   6.365 +			val _ = TextIO.output (outfile,(("subgoals forked to checkChildren: "^prems_string)^prover^thmstring^goalstring^childCmd) )
   6.366 +			val _ =  TextIO.closeOut outfile
   6.367 +		      val childDone = (case prover of
   6.368 +	    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
   6.369 +			   in
   6.370 +			    if childDone      (**********************************************)
   6.371 +			    then              (* child has found a proof and transferred it *)
   6.372 +					      (**********************************************)
   6.373  
   6.374 -                                                       (**********************************************)
   6.375 -                                                       (* Remove this child and go on to check others*)
   6.376 -                                                       (**********************************************)
   6.377 -                                                       ( Unix.reap child_handle;
   6.378 -                                                         checkChildren(otherChildren, toParentStr))
   6.379 -                                                    else 
   6.380 -                                                       (**********************************************)
   6.381 -                                                       (* Keep this child and go on to check others  *)
   6.382 -                                                       (**********************************************)
   6.383 +			       (**********************************************)
   6.384 +			       (* Remove this child and go on to check others*)
   6.385 +			       (**********************************************)
   6.386 +			       ( Unix.reap child_handle;
   6.387 +				 checkChildren(otherChildren, toParentStr))
   6.388 +			    else 
   6.389 +			       (**********************************************)
   6.390 +			       (* Keep this child and go on to check others  *)
   6.391 +			       (**********************************************)
   6.392  
   6.393 -                                                         (childProc::(checkChildren (otherChildren, toParentStr)))
   6.394 -                                                 end
   6.395 -                                               else
   6.396 -                                                   let val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));  
   6.397 -                                                val _ = TextIO.output (outfile,"No child output " )
   6.398 -                                                val _ =  TextIO.closeOut outfile
   6.399 -                                                 in
   6.400 -                                                    (childProc::(checkChildren (otherChildren, toParentStr)))
   6.401 -                                                 end
   6.402 -                                            end
   6.403 +				 (childProc::(checkChildren (otherChildren, toParentStr)))
   6.404 +			 end
   6.405 +		       else
   6.406 +			   let val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));  
   6.407 +			val _ = TextIO.output (outfile,"No child output " )
   6.408 +			val _ =  TextIO.closeOut outfile
   6.409 +			 in
   6.410 +			    (childProc::(checkChildren (otherChildren, toParentStr)))
   6.411 +			 end
   6.412 +		    end
   6.413  
   6.414 -                   
   6.415 -                (********************************************************************)                  
   6.416 -                (* call resolution processes                                        *)
   6.417 -                (* settings should be a list of strings                             *)
   6.418 -                (* e.g. ["-t 300", "-m 100000"]                                     *)
   6.419 -                (* takes list of (string, string, string list, string)list proclist *)
   6.420 -                (********************************************************************)
   6.421 +	     
   6.422 +	  (********************************************************************)                  
   6.423 +	  (* call resolution processes                                        *)
   6.424 +	  (* settings should be a list of strings                             *)
   6.425 +	  (* e.g. ["-t 300", "-m 100000"]                                     *)
   6.426 +	  (* takes list of (string, string, string list, string)list proclist *)
   6.427 +	  (********************************************************************)
   6.428  
   6.429  
   6.430 -  (*** add subgoal id num to this *)
   6.431 -                   fun execCmds  [] procList = procList
   6.432 -                   |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  = 
   6.433 -                                                     if (prover = "spass") 
   6.434 -                                                     then 
   6.435 -                                                         let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   6.436 - 						             val (instr, outstr)=Unix.streamsOf childhandle
   6.437 -                                                             val newProcList =    (((CMDPROC{
   6.438 -            									  prover = prover,
   6.439 -   										  cmd = file,
   6.440 -  									          thmstring = thmstring,
   6.441 -  									          goalstring = goalstring,
   6.442 - 										  proc_handle = childhandle,
   6.443 -									          instr = instr,
   6.444 -   									          outstr = outstr })::procList))
   6.445 -  	                                                      val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "exec_child")));  
   6.446 -                                                val _ = TextIO.output (outfile,"executing command for goal:"^goalstring^proverCmd^(concat settings)^file )
   6.447 -                                                val _ =  TextIO.closeOut outfile
   6.448 -                                                         in
   6.449 -                                                            execCmds cmds newProcList
   6.450 -                                                         end
   6.451 -                                                     else 
   6.452 -                                                         let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   6.453 - 						             val (instr, outstr)=Unix.streamsOf childhandle
   6.454 -							     val newProcList =    (((CMDPROC{
   6.455 -            									  prover = prover,
   6.456 -   										  cmd = file,
   6.457 -  									          thmstring = thmstring,
   6.458 -  									          goalstring = goalstring,
   6.459 - 										  proc_handle = childhandle,
   6.460 -									          instr = instr,
   6.461 -   									          outstr = outstr })::procList))
   6.462 -                                                         in
   6.463 -                                                            execCmds cmds newProcList
   6.464 -                                                         end
   6.465 +(*** add subgoal id num to this *)
   6.466 +	     fun execCmds  [] procList = procList
   6.467 +	     |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  = 
   6.468 +					       if (prover = "spass") 
   6.469 +					       then 
   6.470 +						   let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   6.471 +						       val (instr, outstr)=Unix.streamsOf childhandle
   6.472 +						       val newProcList =    (((CMDPROC{
   6.473 +									    prover = prover,
   6.474 +									    cmd = file,
   6.475 +									    thmstring = thmstring,
   6.476 +									    goalstring = goalstring,
   6.477 +									    proc_handle = childhandle,
   6.478 +									    instr = instr,
   6.479 +									    outstr = outstr })::procList))
   6.480 +							val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "exec_child")));  
   6.481 +					  val _ = TextIO.output (outfile,"executing command for goal:"^goalstring^proverCmd^(concat settings)^file )
   6.482 +					  val _ =  TextIO.closeOut outfile
   6.483 +						   in
   6.484 +						      execCmds cmds newProcList
   6.485 +						   end
   6.486 +					       else 
   6.487 +						   let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   6.488 +						       val (instr, outstr)=Unix.streamsOf childhandle
   6.489 +						       val newProcList =    (((CMDPROC{
   6.490 +									    prover = prover,
   6.491 +									    cmd = file,
   6.492 +									    thmstring = thmstring,
   6.493 +									    goalstring = goalstring,
   6.494 +									    proc_handle = childhandle,
   6.495 +									    instr = instr,
   6.496 +									    outstr = outstr })::procList))
   6.497 +						   in
   6.498 +						      execCmds cmds newProcList
   6.499 +						   end
   6.500  
   6.501  
   6.502  
   6.503 -                (****************************************)                  
   6.504 -                (* call resolution processes remotely   *)
   6.505 -                (* settings should be a list of strings *)
   6.506 -                (* e.g. ["-t 300", "-m 100000"]         *)
   6.507 -                (****************************************)
   6.508 -  
   6.509 -                 (*  fun execRemoteCmds  [] procList = procList
   6.510 -                   |   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
   6.511 -                                             let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   6.512 -                                                 in
   6.513 -                                                      execRemoteCmds  cmds newProcList
   6.514 -                                                 end
   6.515 +	  (****************************************)                  
   6.516 +	  (* call resolution processes remotely   *)
   6.517 +	  (* settings should be a list of strings *)
   6.518 +	  (* e.g. ["-t 300", "-m 100000"]         *)
   6.519 +	  (****************************************)
   6.520 +
   6.521 +	   (*  fun execRemoteCmds  [] procList = procList
   6.522 +	     |   execRemoteCmds ((prover, thmstring,goalstring,proverCmd ,settings,file)::cmds) procList  =  
   6.523 +				       let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,thmstring,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   6.524 +					   in
   6.525 +						execRemoteCmds  cmds newProcList
   6.526 +					   end
   6.527  *)
   6.528  
   6.529 -                   fun printList (outStr, []) = ()
   6.530 -                   |   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
   6.531 +	     fun printList (outStr, []) = ()
   6.532 +	     |   printList (outStr, (x::xs)) = (TextIO.output (outStr, x);TextIO.flushOut outStr; printList (outStr,xs))                  
   6.533  
   6.534  
   6.535 -                (**********************************************)                  
   6.536 -                (* Watcher Loop                               *)
   6.537 -                (**********************************************)
   6.538 +	  (**********************************************)                  
   6.539 +	  (* Watcher Loop                               *)
   6.540 +	  (**********************************************)
   6.541 +
   6.542  
   6.543  
   6.544  
   6.545 -   
   6.546 -                    fun keepWatching (toParentStr, fromParentStr,procList) = 
   6.547 -                          let    fun loop (procList) =  
   6.548 -                                 (
   6.549 -                                 let val cmdsFromIsa = pollParentInput ()
   6.550 -                                     fun killchildHandler (n:int)  = (TextIO.output(toParentStr, "Killing child proof processes!\n");
   6.551 -                                                  TextIO.flushOut toParentStr;
   6.552 -                                                   killChildren (map (cmdchildHandle) procList);
   6.553 -                                                    ())
   6.554 -                                     
   6.555 -                                 in 
   6.556 -                                    (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
   6.557 -                                                                                       (**********************************)
   6.558 -                                    if (isSome cmdsFromIsa) then                       (*  deal with input from Isabelle *)
   6.559 -                                         (                                             (**********************************)                             
   6.560 -                                          if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
   6.561 -                                          then 
   6.562 -                                            (
   6.563 -                                              let val child_handles = map cmdchildHandle procList 
   6.564 -                                              in
   6.565 -                                                 killChildren child_handles;
   6.566 -                                                 (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)                                                              loop ([])
   6.567 -                                              end
   6.568 -                                                 
   6.569 -                                             )
   6.570 -                                          else
   6.571 -                                            ( 
   6.572 -                                              if ((length procList)<10)    (********************)
   6.573 -                                              then                        (* Execute locally  *)
   6.574 -                                                 (                        (********************)
   6.575 -                                                  let 
   6.576 -                                                    val newProcList = execCmds (valOf cmdsFromIsa) procList
   6.577 -                                                    val parentID = Posix.ProcEnv.getppid()
   6.578 -                                                    val newProcList' =checkChildren (newProcList, toParentStr) 
   6.579 -                                                  in
   6.580 -                                                    (*Posix.Process.sleep (Time.fromSeconds 1);*)
   6.581 -                                                    loop (newProcList') 
   6.582 -                                                  end
   6.583 -                                                  )
   6.584 -                                              else                         (*********************************)
   6.585 -                                                                           (* Execute remotely              *)
   6.586 - 									   (* (actually not remote for now )*)
   6.587 -                                                  (                        (*********************************)
   6.588 -                                                  let 
   6.589 -                                                    val newProcList = execCmds (valOf cmdsFromIsa) procList
   6.590 -                                                    val parentID = Posix.ProcEnv.getppid()
   6.591 -                                                    val newProcList' =checkChildren (newProcList, toParentStr) 
   6.592 -                                                  in
   6.593 -                                                    (*Posix.Process.sleep (Time.fromSeconds 1);*)
   6.594 -                                                    loop (newProcList') 
   6.595 -                                                  end
   6.596 -                                                  )
   6.597 +	      fun keepWatching (toParentStr, fromParentStr,procList) = 
   6.598 +		    let    fun loop (procList) =  
   6.599 +			   (
   6.600 +			   let val cmdsFromIsa = pollParentInput ()
   6.601 +			       fun killchildHandler (n:int)  = (TextIO.output(toParentStr, "Killing child proof processes!\n");
   6.602 +					    TextIO.flushOut toParentStr;
   6.603 +					     killChildren (map (cmdchildHandle) procList);
   6.604 +					      ())
   6.605 +			       
   6.606 +			   in 
   6.607 +			      (*Signal.signal (Posix.Signal.usr2, Signal.SIG_HANDLE killchildHandler);*)
   6.608 +										 (**********************************)
   6.609 +			      if (isSome cmdsFromIsa) then                       (*  deal with input from Isabelle *)
   6.610 +				   (                                             (**********************************)                             
   6.611 +				    if (getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" )
   6.612 +				    then 
   6.613 +				      (
   6.614 +					let val child_handles = map cmdchildHandle procList 
   6.615 +					in
   6.616 +					   killChildren child_handles;
   6.617 +					   (*Posix.Process.kill(Posix.Process.K_PROC (Posix.ProcEnv.getppid()), Posix.Signal.usr2);*)                                                              loop ([])
   6.618 +					end
   6.619 +					   
   6.620 +				       )
   6.621 +				    else
   6.622 +				      ( 
   6.623 +					if ((length procList)<10)    (********************)
   6.624 +					then                        (* Execute locally  *)
   6.625 +					   (                        (********************)
   6.626 +					    let 
   6.627 +					      val newProcList = execCmds (valOf cmdsFromIsa) procList
   6.628 +					      val parentID = Posix.ProcEnv.getppid()
   6.629 +					      val newProcList' =checkChildren (newProcList, toParentStr) 
   6.630 +					    in
   6.631 +					      (*Posix.Process.sleep (Time.fromSeconds 1);*)
   6.632 +					      loop (newProcList') 
   6.633 +					    end
   6.634 +					    )
   6.635 +					else                         (*********************************)
   6.636 +								     (* Execute remotely              *)
   6.637 +								     (* (actually not remote for now )*)
   6.638 +					    (                        (*********************************)
   6.639 +					    let 
   6.640 +					      val newProcList = execCmds (valOf cmdsFromIsa) procList
   6.641 +					      val parentID = Posix.ProcEnv.getppid()
   6.642 +					      val newProcList' =checkChildren (newProcList, toParentStr) 
   6.643 +					    in
   6.644 +					      (*Posix.Process.sleep (Time.fromSeconds 1);*)
   6.645 +					      loop (newProcList') 
   6.646 +					    end
   6.647 +					    )
   6.648  
   6.649  
   6.650  
   6.651 -                                              )
   6.652 -                                           )                                              (******************************)
   6.653 -                                    else                                                  (* No new input from Isabelle *)
   6.654 -                                                                                          (******************************)
   6.655 -                                        (    let val newProcList = checkChildren ((procList), toParentStr)
   6.656 -                                             in
   6.657 -                                               Posix.Process.sleep (Time.fromSeconds 1);
   6.658 -                                               loop (newProcList)
   6.659 -                                             end
   6.660 -                                         
   6.661 -                                         )
   6.662 -                                  end)
   6.663 -                          in  
   6.664 -                              loop (procList)
   6.665 -                          end
   6.666 -                      
   6.667 -          
   6.668 -                      in
   6.669 -                       (***************************)
   6.670 -                       (*** Sort out pipes ********)
   6.671 -                       (***************************)
   6.672 +					)
   6.673 +				     )                                              (******************************)
   6.674 +			      else                                                  (* No new input from Isabelle *)
   6.675 +										    (******************************)
   6.676 +				  (    let val newProcList = checkChildren ((procList), toParentStr)
   6.677 +				       in
   6.678 +					 Posix.Process.sleep (Time.fromSeconds 1);
   6.679 +					 loop (newProcList)
   6.680 +				       end
   6.681 +				   
   6.682 +				   )
   6.683 +			    end)
   6.684 +		    in  
   6.685 +			loop (procList)
   6.686 +		    end
   6.687 +		
   6.688 +    
   6.689 +		in
   6.690 +		 (***************************)
   6.691 +		 (*** Sort out pipes ********)
   6.692 +		 (***************************)
   6.693  
   6.694 -			Posix.IO.close (#outfd p1);
   6.695 -			Posix.IO.close (#infd p2);
   6.696 -			Posix.IO.dup2{old = oldchildin, new = fromParent};
   6.697 -                        Posix.IO.close oldchildin;
   6.698 -			Posix.IO.dup2{old = oldchildout, new = toParent};
   6.699 -                        Posix.IO.close oldchildout;
   6.700 +		  Posix.IO.close (#outfd p1);
   6.701 +		  Posix.IO.close (#infd p2);
   6.702 +		  Posix.IO.dup2{old = oldchildin, new = fromParent};
   6.703 +		  Posix.IO.close oldchildin;
   6.704 +		  Posix.IO.dup2{old = oldchildout, new = toParent};
   6.705 +		  Posix.IO.close oldchildout;
   6.706  
   6.707 -                        (***************************)
   6.708 -                        (* start the watcher loop  *)
   6.709 -                        (***************************)
   6.710 -                        keepWatching (toParentStr, fromParentStr, procList);
   6.711 +		  (***************************)
   6.712 +		  (* start the watcher loop  *)
   6.713 +		  (***************************)
   6.714 +		  keepWatching (toParentStr, fromParentStr, procList);
   6.715  
   6.716  
   6.717 -                        (****************************************************************************)
   6.718 -                        (* fake return value - actually want the watcher to loop until killed       *)
   6.719 -                        (****************************************************************************)
   6.720 -                        Posix.Process.wordToPid 0w0
   6.721 -			
   6.722 -		      end);
   6.723 -		(* end case *)
   6.724 +		  (****************************************************************************)
   6.725 +		  (* fake return value - actually want the watcher to loop until killed       *)
   6.726 +		  (****************************************************************************)
   6.727 +		  Posix.Process.wordToPid 0w0
   6.728 +		  
   6.729 +		end);
   6.730 +	  (* end case *)
   6.731  
   6.732  
   6.733 -          val _ = TextIO.flushOut TextIO.stdOut
   6.734 +    val _ = TextIO.flushOut TextIO.stdOut
   6.735  
   6.736 -          (*******************************)
   6.737 -          (***  set watcher going ********)
   6.738 -          (*******************************)
   6.739 +    (*******************************)
   6.740 +    (***  set watcher going ********)
   6.741 +    (*******************************)
   6.742  
   6.743 -          val procList = []
   6.744 -          val pid = startWatcher (procList)
   6.745 -          (**************************************************)
   6.746 -          (* communication streams to watcher               *)
   6.747 -          (**************************************************)
   6.748 +    val procList = []
   6.749 +    val pid = startWatcher (procList)
   6.750 +    (**************************************************)
   6.751 +    (* communication streams to watcher               *)
   6.752 +    (**************************************************)
   6.753  
   6.754 -	  val instr = openInFD ("_exec_in", #infd p2)
   6.755 -          val outstr = openOutFD ("_exec_out", #outfd p1)
   6.756 -          
   6.757 -          in
   6.758 -           (*******************************)
   6.759 -           (* close the child-side fds    *)
   6.760 -           (*******************************)
   6.761 -            Posix.IO.close (#outfd p2);
   6.762 -            Posix.IO.close (#infd p1);
   6.763 -            (* set the fds close on exec *)
   6.764 -            Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   6.765 -            Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   6.766 -             
   6.767 -           (*******************************)
   6.768 -           (* return value                *)
   6.769 -           (*******************************)
   6.770 -            PROC{pid = pid,
   6.771 -              instr = instr,
   6.772 -              outstr = outstr
   6.773 -            }
   6.774 -         end;
   6.775 +    val instr = openInFD ("_exec_in", #infd p2)
   6.776 +    val outstr = openOutFD ("_exec_out", #outfd p1)
   6.777 +    
   6.778 +    in
   6.779 +     (*******************************)
   6.780 +     (* close the child-side fds    *)
   6.781 +     (*******************************)
   6.782 +      Posix.IO.close (#outfd p2);
   6.783 +      Posix.IO.close (#infd p1);
   6.784 +      (* set the fds close on exec *)
   6.785 +      Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   6.786 +      Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   6.787 +       
   6.788 +     (*******************************)
   6.789 +     (* return value                *)
   6.790 +     (*******************************)
   6.791 +      PROC{pid = pid,
   6.792 +	instr = instr,
   6.793 +	outstr = outstr
   6.794 +      }
   6.795 +   end;
   6.796  
   6.797  
   6.798  
     7.1 --- a/src/HOL/Tools/res_atp.ML	Tue May 24 07:43:38 2005 +0200
     7.2 +++ b/src/HOL/Tools/res_atp.ML	Tue May 24 10:23:24 2005 +0200
     7.3 @@ -245,19 +245,18 @@
     7.4  (**********************************************)
     7.5  
     7.6  fun isar_atp_goal' thm k n tfree_lits  (childin, childout, pid) = 
     7.7 -                  	if (k > n) 
     7.8 -                        then () 
     7.9 -	  		else 
    7.10 -                           (let val  prems = prems_of thm 
    7.11 -                                val sg_term = get_nth n prems
    7.12 -                                val thmstring = string_of_thm thm
    7.13 -                            in   
    7.14 -                                 
    7.15 -                		(warning("in isar_atp_goal'"));
    7.16 -                                (warning("thmstring in isar_atp_goal': "^thmstring));
    7.17 - 				 isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; 
    7.18 -                                 isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) 
    7.19 -                            end);
    7.20 +      if (k > n) 
    7.21 +      then () 
    7.22 +      else 
    7.23 +	  let val  prems = prems_of thm 
    7.24 +	      val sg_term = ReconOrderClauses.get_nth n prems
    7.25 +	      val thmstring = string_of_thm thm
    7.26 +	  in   
    7.27 +	      (warning("in isar_atp_goal'"));
    7.28 +	      (warning("thmstring in isar_atp_goal': "^thmstring));
    7.29 +	       isar_atp_g tfree_lits  sg_term (childin, childout, pid) k thm; 
    7.30 +	       isar_atp_goal' thm (k+1) n tfree_lits  (childin, childout, pid) 
    7.31 +	  end;
    7.32  
    7.33  
    7.34  fun isar_atp_goal thm n_subgoals tfree_lits   (childin, childout, pid) =