src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 17997 6c0fe78624d9
parent 17775 2679ba74411f
child 18700 f04a8755d6ca
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Oct 27 13:59:06 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Thu Oct 27 18:25:33 2005 +0200
     1.3 @@ -157,8 +157,10 @@
     1.4      end
     1.5  
     1.6  (* get names of clasimp axioms used*)
     1.7 - fun get_axiom_names step_nums clause_arr =
     1.8 -   map (ResClause.get_axiomName o #1) (get_clasimp_cls clause_arr step_nums);   
     1.9 +fun get_axiom_names step_nums clause_arr =
    1.10 +  distinct (sort_strings 
    1.11 +            (map (ResClause.get_axiomName o #1) 
    1.12 +	     (get_clasimp_cls clause_arr step_nums)));   
    1.13  
    1.14  fun get_axiom_names_spass proofstr clause_arr =
    1.15    let (* parse spass proof into datatype *)