diff -r e6f1ff40ba99 -r b338c218cc6e src/HOL/Tools/ATP/recon_transfer_proof.ML
--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Mar 07 03:59:48 2006 +0100
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Tue Mar 07 04:01:25 2006 +0100
@@ -149,17 +149,17 @@
 
 (* retrieve the axioms that were obtained from the clasimpset *)
 
-fun get_clasimp_cls (clause_arr: (ResClause.clause * thm) array) step_nums = 
-    let val clasimp_nums = List.filter (is_clasimp_ax (Array.length clause_arr - 1)) 
+fun get_clasimp_cls (names_arr: string array) step_nums = 
+    let val clasimp_nums = List.filter (is_clasimp_ax (Array.length names_arr - 1)) 
 	                   (map subone step_nums)
     in
-	map (fn x =>  Array.sub(clause_arr, x)) clasimp_nums
+	map (fn x =>  Array.sub(names_arr, x)) clasimp_nums
     end
 
 (* get names of clasimp axioms used*)
-fun get_axiom_names step_nums clause_arr =
+fun get_axiom_names step_nums names_arr =
   sort_distinct string_ord
-    (map (ResClause.get_axiomName o #1) (get_clasimp_cls clause_arr step_nums));
+    (get_clasimp_cls names_arr step_nums);
 
  (*String contains multiple lines. We want those of the form 
      "253[0:Inp] et cetera..."
@@ -171,8 +171,8 @@
       val lines = String.tokens (fn c => c = #"\n") proofstr
   in  List.mapPartial (inputno o toks) lines  end
 
-fun get_axiom_names_spass proofstr clause_arr  =
-   get_axiom_names (get_spass_linenums proofstr) clause_arr;
+fun get_axiom_names_spass proofstr names_arr  =
+   get_axiom_names (get_spass_linenums proofstr) names_arr;
     
  (*String contains multiple lines.
   A list consisting of the first number in each line is returned. *)
@@ -183,8 +183,8 @@
       val lines = String.tokens (fn c => c = #"\n") proofstr
   in  List.mapPartial (firstno o numerics) lines  end
 
-fun get_axiom_names_e proofstr clause_arr  =
-   get_axiom_names (get_linenums proofstr) clause_arr;
+fun get_axiom_names_e proofstr names_arr  =
+   get_axiom_names (get_linenums proofstr) names_arr;
     
  (*String contains multiple lines. We want those of the form 
      "*********** [448, input] ***********".
@@ -196,8 +196,8 @@
       val lines = String.tokens (fn c => c = #"\n") proofstr
   in  List.mapPartial (inputno o toks) lines  end
 
-fun get_axiom_names_vamp proofstr clause_arr  =
-   get_axiom_names (get_vamp_linenums proofstr) clause_arr;
+fun get_axiom_names_vamp proofstr names_arr  =
+   get_axiom_names (get_vamp_linenums proofstr) names_arr;
     
 
 (***********************************************)
@@ -212,7 +212,7 @@
 
 fun addvars c (a,b)  = (a,b,c)
 
-fun get_axioms_used proof_steps thms clause_arr  =
+fun get_axioms_used proof_steps thms names_arr  =
  let val axioms = (List.filter is_axiom) proof_steps
      val step_nums = get_step_nums axioms []
 
@@ -265,12 +265,12 @@
 
 
 (*The signal handler in watcher.ML must be able to read the output of this.*)
-fun prover_lemma_list_aux getax proofstr probfile toParent ppid clause_arr = 
+fun prover_lemma_list_aux getax proofstr probfile toParent ppid names_arr = 
  let val _ = trace
                ("\n\nGetting lemma names. proofstr is " ^ proofstr ^
                 "\nprobfile is " ^ probfile ^
-                "  num of clauses is " ^ string_of_int (Array.length clause_arr))
-     val axiom_names = getax proofstr clause_arr
+                "  num of clauses is " ^ string_of_int (Array.length names_arr))
+     val axiom_names = getax proofstr names_arr
      val ax_str = rules_to_string axiom_names
     in 
 	 trace ("\nDone. Lemma list is " ^ ax_str);
@@ -298,7 +298,7 @@
 
 (**** Full proof reconstruction for SPASS (not really working) ****)
 
-fun spass_reconstruct proofstr probfile toParent ppid thms clause_arr = 
+fun spass_reconstruct proofstr probfile toParent ppid thms names_arr = 
   let val _ = trace ("\nspass_reconstruct. Proofstr is "^proofstr)
       val tokens = #1(lex proofstr)
 
@@ -315,7 +315,7 @@
       (* subgoal this is, and turn it into meta_clauses *)
       (* should prob add array and table here, so that we can get axioms*)
       (* produced from the clasimpset rather than the problem *)
-      val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms clause_arr
+      val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps  thms names_arr
       
       (*val numcls_string = numclstr ( vars, numcls) ""*)
       val _ = trace "\ngot axioms"