src/HOL/Tools/ATP/recon_transfer_proof.ML
changeset 19046 bc5c6c9b114e
parent 18797 8559cc115673
child 19199 b338c218cc6e
     1.1 --- a/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Feb 15 19:11:10 2006 +0100
     1.2 +++ b/src/HOL/Tools/ATP/recon_transfer_proof.ML	Wed Feb 15 21:34:55 2006 +0100
     1.3 @@ -158,9 +158,8 @@
     1.4  
     1.5  (* get names of clasimp axioms used*)
     1.6  fun get_axiom_names step_nums clause_arr =
     1.7 -  distinct (sort_strings 
     1.8 -            (map (ResClause.get_axiomName o #1) 
     1.9 -	     (get_clasimp_cls clause_arr step_nums)));   
    1.10 +  sort_distinct string_ord
    1.11 +    (map (ResClause.get_axiomName o #1) (get_clasimp_cls clause_arr step_nums));
    1.12  
    1.13   (*String contains multiple lines. We want those of the form 
    1.14       "253[0:Inp] et cetera..."
    1.15 @@ -221,13 +220,13 @@
    1.16       
    1.17       val vars = map thm_vars clauses
    1.18      
    1.19 -     val distvars = distinct (fold append vars [])
    1.20 +     val distvars = distinct (op =) (fold append vars [])
    1.21       val clause_terms = map prop_of clauses  
    1.22       val clause_frees = List.concat (map term_frees clause_terms)
    1.23  
    1.24       val frees = map lit_string_with_nums clause_frees;
    1.25  
    1.26 -     val distfrees = distinct frees
    1.27 +     val distfrees = distinct (op =) frees
    1.28  
    1.29       val metas = map Meson.make_meta_clause clauses
    1.30       val ax_strs = map #3 axioms