# HG changeset patch
# User wenzelm
# Date 1154287731 -7200
# Node ID 5eda3b38ec9073cb993885861fe899316104c9dc
# Parent  4fe3c0911907e0851c76cf1f2d7e4b5157d1555f
removed unused add_in_order/add_once (cf. OrdList.insert);

diff -r 4fe3c0911907 -r 5eda3b38ec90 src/HOL/Tools/ATP/recon_translate_proof.ML
--- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Sun Jul 30 21:28:50 2006 +0200
+++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Sun Jul 30 21:28:51 2006 +0200
@@ -6,16 +6,6 @@
 structure ReconTranslateProof =
 struct
 
-fun add_in_order (x:string) [] = [x]
-|   add_in_order (x:string) ((y:string)::ys) = if (x < y) 
-                             then 
-                                  (x::(y::ys))
-                             else
-                                  (y::(add_in_order x ys))
-fun add_once x [] = [x]
-|   add_once x (y::ys) = if x mem (y::ys) then (y::ys)
-                         else add_in_order x (y::ys)
-     
 fun thm_vars thm = map (fn ((name,ix),_) => name) (Drule.vars_of thm);
 
 exception Reflex_equal;