removed unused add_in_order/add_once (cf. OrdList.insert);
--- 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;