removed unused add_in_order/add_once (cf. OrdList.insert);
authorwenzelm
Sun, 30 Jul 2006 21:28:51 +0200
changeset 20259 5eda3b38ec90
parent 20258 4fe3c0911907
child 20260 990dbc007ca6
removed unused add_in_order/add_once (cf. OrdList.insert);
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;