# HG changeset patch # User paulson # Date 1109930284 -3600 # Node ID 9c89b1adf573c10fd965be8ac10fd2398e9d2485 # Parent c166086feace8c71808c98ecf2b3e13ba5af02fa removed dead code diff -r c166086feace -r 9c89b1adf573 src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Thu Mar 03 17:22:46 2005 +0100 +++ b/src/HOL/Tools/res_atp.ML Fri Mar 04 10:58:04 2005 +0100 @@ -151,16 +151,6 @@ local -fun retr_thms ([]:MetaSimplifier.rrule list) = [] - | retr_thms (r::rs) = (#thm r)::(retr_thms rs); - - -fun snds [] = [] - | snds ((x,y)::l) = y::(snds l); - - - - fun get_thms_cs claset = let val clsset = rep_cs claset val safeEs = #safeEs clsset