src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 17569 c1143a96f6d7
parent 17488 67376a311a2b
child 17583 c272b91b619f
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Sep 21 18:35:19 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Sep 21 18:35:31 2005 +0200
     1.3 @@ -189,7 +189,7 @@
     1.4      get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) clause_arr
     1.5    end;
     1.6      
     1.7 - (*String contains multiple lines, terminated with newline characters.
     1.8 + (*String contains multiple lines.
     1.9    A list consisting of the first number in each line is returned. *)
    1.10  fun get_linenums proofstr = 
    1.11    let val numerics = String.tokens (not o Char.isDigit)
    1.12 @@ -198,9 +198,22 @@
    1.13        val lines = String.tokens (fn c => c = #"\n") proofstr
    1.14    in  List.mapPartial (firstno o numerics) lines  end
    1.15  
    1.16 -fun get_axiom_names_vamp_E proofstr clause_arr  =
    1.17 +fun get_axiom_names_e proofstr clause_arr  =
    1.18     get_axiom_names (get_linenums proofstr) clause_arr;
    1.19      
    1.20 + (*String contains multiple lines. We want those of the form 
    1.21 +     "*********** [448, input] ***********".
    1.22 +  A list consisting of the first number in each line is returned. *)
    1.23 +fun get_vamp_linenums proofstr = 
    1.24 +  let val toks = String.tokens (not o Char.isAlphaNum)
    1.25 +      fun inputno [n,"input"] = Int.fromString n
    1.26 +        | inputno _ = NONE
    1.27 +      val lines = String.tokens (fn c => c = #"\n") proofstr
    1.28 +  in  List.mapPartial (inputno o toks) lines  end
    1.29 +
    1.30 +fun get_axiom_names_vamp proofstr clause_arr  =
    1.31 +   get_axiom_names (get_vamp_linenums proofstr) clause_arr;
    1.32 +    
    1.33  
    1.34  (***********************************************)
    1.35  (* get axioms for reconstruction               *)
    1.36 @@ -303,7 +316,9 @@
    1.37        (* Attempt to prevent several signals from turning up simultaneously *)
    1.38        Posix.Process.sleep(Time.fromSeconds 1); ());
    1.39  
    1.40 -val prover_lemma_list = prover_lemma_list_aux get_axiom_names_vamp_E;
    1.41 +val e_lemma_list = prover_lemma_list_aux get_axiom_names_e;
    1.42 +
    1.43 +val vamp_lemma_list = prover_lemma_list_aux get_axiom_names_vamp;
    1.44  
    1.45  val spass_lemma_list = prover_lemma_list_aux get_axiom_names_spass;
    1.46