src/HOL/Tools/res_atp.ML
changeset 18404 aa27c10a040e
parent 18270 27227433cb42
child 18675 333a73034023
     1.1 --- a/src/HOL/Tools/res_atp.ML	Wed Dec 14 06:19:33 2005 +0100
     1.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Dec 14 16:13:09 2005 +0100
     1.3 @@ -52,16 +52,6 @@
     1.4  
     1.5  (**** For running in Isar ****)
     1.6  
     1.7 -(* same function as that in res_axioms.ML *)
     1.8 -fun repeat_RS thm1 thm2 =
     1.9 -    let val thm1' =  thm1 RS thm2 handle THM _ => thm1
    1.10 -    in
    1.11 -        if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
    1.12 -    end;
    1.13 -
    1.14 -(* a special version of repeat_RS *)
    1.15 -fun repeat_someI_ex th = repeat_RS th someI_ex;
    1.16 -
    1.17  fun writeln_strs _   []      = ()
    1.18    | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
    1.19