src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 17488 67376a311a2b
parent 17484 f6a225f97f0a
child 17569 c1143a96f6d7
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon Sep 19 16:42:11 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Mon Sep 19 18:30:22 2005 +0200
     1.3 @@ -158,7 +158,7 @@
     1.4  (* get names of clasimp axioms used                  *)
     1.5  (*****************************************************)
     1.6  
     1.7 - fun get_axiom_names step_nums thms clause_arr =
     1.8 + fun get_axiom_names step_nums clause_arr =
     1.9     let 
    1.10       (* not sure why this is necessary again, but seems to be *)
    1.11        val _ = (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"])))
    1.12 @@ -177,7 +177,7 @@
    1.13     end
    1.14     
    1.15  
    1.16 -fun get_axiom_names_spass proofstr thms clause_arr =
    1.17 +fun get_axiom_names_spass proofstr clause_arr =
    1.18    let (* parse spass proof into datatype *)
    1.19        val _ = File.write (File.tmp_path (Path.basic "parsing_progress")) 
    1.20                           ("Started parsing:\n" ^ proofstr)
    1.21 @@ -186,8 +186,7 @@
    1.22        val _ = File.append (File.tmp_path (Path.basic "parsing_progress")) "\nFinished!"
    1.23        (* get axioms as correctly numbered clauses w.r.t. the Spass proof *)
    1.24    in
    1.25 -    get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) 
    1.26 -                    thms clause_arr
    1.27 +    get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) clause_arr
    1.28    end;
    1.29      
    1.30   (*String contains multiple lines, terminated with newline characters.
    1.31 @@ -199,8 +198,8 @@
    1.32        val lines = String.tokens (fn c => c = #"\n") proofstr
    1.33    in  List.mapPartial (firstno o numerics) lines  end
    1.34  
    1.35 -fun get_axiom_names_vamp_E proofstr thms clause_arr  =
    1.36 -   get_axiom_names (get_linenums proofstr) thms clause_arr;
    1.37 +fun get_axiom_names_vamp_E proofstr clause_arr  =
    1.38 +   get_axiom_names (get_linenums proofstr) clause_arr;
    1.39      
    1.40  
    1.41  (***********************************************)
    1.42 @@ -274,13 +273,12 @@
    1.43  val restore_linebreaks = subst_for #"\t" #"\n";
    1.44  
    1.45  
    1.46 -fun prover_lemma_list_aux proofstr goalstring toParent ppid thms clause_arr getax = 
    1.47 +fun prover_lemma_list_aux getax proofstr goalstring toParent ppid clause_arr = 
    1.48   let val _ = File.append(File.tmp_path (Path.basic "prover_lemmastring"))
    1.49                 ("proofstr is " ^ proofstr ^
    1.50                  "\ngoalstr is " ^ goalstring ^
    1.51                  "\nnum of clauses is " ^ string_of_int (Array.length clause_arr))
    1.52 -
    1.53 -     val axiom_names = getax proofstr thms clause_arr
    1.54 +     val axiom_names = getax proofstr clause_arr
    1.55       val ax_str = rules_to_string axiom_names
    1.56      in 
    1.57  	 File.append(File.tmp_path (Path.basic "prover_lemmastring"))
    1.58 @@ -292,7 +290,7 @@
    1.59  
    1.60  	 Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.61  	(* Attempt to prevent several signals from turning up simultaneously *)
    1.62 -	 Posix.Process.sleep(Time.fromSeconds 1) ; all_tac
    1.63 +	 Posix.Process.sleep(Time.fromSeconds 1); ()
    1.64      end
    1.65      handle exn => (*FIXME: exn handler is too general!*)
    1.66       (File.write(File.tmp_path (Path.basic "proverString_handler")) 
    1.67 @@ -303,15 +301,11 @@
    1.68        TextIO.flushOut toParent;
    1.69        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2);
    1.70        (* Attempt to prevent several signals from turning up simultaneously *)
    1.71 -      Posix.Process.sleep(Time.fromSeconds 1); all_tac);
    1.72 +      Posix.Process.sleep(Time.fromSeconds 1); ());
    1.73  
    1.74 -fun prover_lemma_list proofstr goalstring toParent ppid thms clause_arr  = 
    1.75 -  prover_lemma_list_aux proofstr goalstring toParent ppid thms        
    1.76 -       clause_arr get_axiom_names_vamp_E;
    1.77 +val prover_lemma_list = prover_lemma_list_aux get_axiom_names_vamp_E;
    1.78  
    1.79 -fun spass_lemma_list proofstr goalstring toParent ppid thms clause_arr = 
    1.80 -  prover_lemma_list_aux proofstr goalstring toParent ppid thms        
    1.81 -       clause_arr get_axiom_names_spass;
    1.82 +val spass_lemma_list = prover_lemma_list_aux get_axiom_names_spass;
    1.83  
    1.84  
    1.85  (**** Full proof reconstruction for SPASS (not really working) ****)