diff -r 1c1d40ff875a -r bb2acfed8212 src/HOL/Tools/ATP/recon_transfer_proof.ML
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Apr 15 17:03:35 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Fri Apr 15 18:16:05 2005 +0200
@@ -108,9 +108,6 @@
 
 
 
-
-
-
 fun is_axiom ( num:int,Axiom, str) = true
 |   is_axiom (num, _,_) = false
 
@@ -128,8 +125,7 @@
 |   get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))])
 *)
 (*FIX - should this have vars in it? *)
-fun there_out_of_order xs ys = let val foo = (checkorder xs ys [] ([],[],[])) 
-                                   
+fun there_out_of_order xs ys = let val foo = (checkorder xs ys [] ([],[],[]))                        
                                in 
                                    true
                               end
@@ -155,9 +151,6 @@
 fun thmstrings [] str = str
 |   thmstrings (x::xs) str = thmstrings xs (str^(string_of_thm x))
 
-fun onelist [] newlist = newlist
-|   onelist (x::xs) newlist = onelist xs (newlist@x)
-
 
  fun get_axioms_used proof_steps thmstring = let 
                                              val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_ax_thmstr")))                                                                      
@@ -175,7 +168,7 @@
                                            
                                             val distvars = distinct (fold append vars [])
                                             val clause_terms = map prop_of clauses  
-                                            val clause_frees = onelist (map term_frees clause_terms) []
+                                            val clause_frees = List.concat (map term_frees clause_terms)
 
                                             val frees = map lit_string_with_nums clause_frees;
 
@@ -313,7 +306,7 @@
                                                   val _ = TextIO.output (outfile, (thmstring))
                                                   val _ =  TextIO.closeOut outfile
                                                   val proofextract = extract_proof proofstr
-                                                  val tokens = fst(lex proofextract)
+                                                  val tokens = #1(lex proofextract)
                                                      
                                               (***********************************)
                                               (* parse spass proof into datatype *)
@@ -352,8 +345,8 @@
                                                   (* turn the proof into a string *)
                                                   val reconProofStr = proofs_to_string proof ""
                                                   (* do the bit for the Isabelle ordered axioms at the top *)
-                                                  val ax_nums = map fst numcls
-                                                  val ax_strs = map get_meta_lits_bracket (map snd numcls)
+                                                  val ax_nums = map #1 numcls
+                                                  val ax_strs = map get_meta_lits_bracket (map #2 numcls)
                                                   val numcls_strs = zip ax_nums ax_strs
                                                   val num_cls_vars =  map (addvars vars) numcls_strs;
                                                   val reconIsaAxStr = origAxs_to_string (zip ax_nums ax_with_vars) ""
@@ -449,7 +442,7 @@
 
 
  val number_list_step =
-        ( number ++ many ((a (Other ",") ++ number)>> snd))
+        ( number ++ many ((a (Other ",") ++ number)>> #2))
         >> (fn (a,b) => (a::b))
         
  val numberlist_step = a (Other "[")  ++ a (Other "]")
@@ -510,9 +503,9 @@
     
  val lines_step = many linestep
 
- val alllines_step = (term_lists_step ++ lines_step ) ++ finished >> fst
+ val alllines_step = (term_lists_step ++ lines_step ) ++ finished >> #1
     
- val parse_step = fst o alllines_step
+ val parse_step = #1 o alllines_step
 
 
  (*
@@ -702,7 +695,7 @@
 val thmstring = " (ALL xa::'a::type.   (~ (P::'a::type => bool) (x::'a::type) | P xa) & (~ P xa | P x)) & (((P::'a::type => bool) (xa::'a::type) | (ALL x::'a::type. P x)) &((ALL x::'a::type. ~ P x) | ~ P (xb::'a::type)))";
 *)
 
-fun apply_res_thm str goalstring  = let val tokens = fst (lex str);
+fun apply_res_thm str goalstring  = let val tokens = #1 (lex str);
 
                                    val (frees,recon_steps) = parse_step tokens 
                                    val isar_str = to_isar_proof (frees, recon_steps, goalstring)