--- a/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Oct 27 13:59:06 2005 +0200
+++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML Thu Oct 27 18:25:33 2005 +0200
@@ -157,8 +157,10 @@
end
(* get names of clasimp axioms used*)
- fun get_axiom_names step_nums clause_arr =
- map (ResClause.get_axiomName o #1) (get_clasimp_cls clause_arr step_nums);
+fun get_axiom_names step_nums clause_arr =
+ distinct (sort_strings
+ (map (ResClause.get_axiomName o #1)
+ (get_clasimp_cls clause_arr step_nums)));
fun get_axiom_names_spass proofstr clause_arr =
let (* parse spass proof into datatype *)