# HG changeset patch
# User paulson
# Date 1134573189 -3600
# Node ID aa27c10a040e955b4bb2541a37f9c63cf6b37a44
# Parent  df0c0f35c897b43b891f92837b90ac2cc0102f67
removed unused function repeat_RS

diff -r df0c0f35c897 -r aa27c10a040e src/HOL/Tools/res_atp.ML
--- a/src/HOL/Tools/res_atp.ML	Wed Dec 14 06:19:33 2005 +0100
+++ b/src/HOL/Tools/res_atp.ML	Wed Dec 14 16:13:09 2005 +0100
@@ -52,16 +52,6 @@
 
 (**** For running in Isar ****)
 
-(* same function as that in res_axioms.ML *)
-fun repeat_RS thm1 thm2 =
-    let val thm1' =  thm1 RS thm2 handle THM _ => thm1
-    in
-        if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
-    end;
-
-(* a special version of repeat_RS *)
-fun repeat_someI_ex th = repeat_RS th someI_ex;
-
 fun writeln_strs _   []      = ()
   | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
 
diff -r df0c0f35c897 -r aa27c10a040e src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Wed Dec 14 06:19:33 2005 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Wed Dec 14 16:13:09 2005 +0100
@@ -25,7 +25,6 @@
   val clause_setup : (theory -> theory) list
   val meson_method_setup : (theory -> theory) list
   val pairname : thm -> (string * thm)
-  val repeat_RS : thm -> thm -> thm
   val cnf_axiom_aux : thm -> thm list
   val cnf_rules1 : (string * thm) list -> string list -> (string * thm list) list * string list
   val cnf_rules2 : (string * thm) list -> string list -> (string * term list) list * string list
@@ -58,8 +57,6 @@
 fun add_EX tm [] = tm
   | add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs;
 
-
-
 fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) (Const("Trueprop",_) $ Free(q,_)) = (p = q)
   | is_neg _ _ = false;
 
@@ -136,13 +133,6 @@
 
 (**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
 
-(* repeated resolution *)
-fun repeat_RS thm1 thm2 =
-    let val thm1' =  thm1 RS thm2 handle THM _ => thm1
-    in
-	if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
-    end;
-
 
 (*Transfer a theorem into theory Reconstruction.thy if it is not already
   inside that theory -- because it's needed for Skolemization *)
@@ -265,9 +255,6 @@
        |> transform_elim |> Drule.freeze_all
        |> ObjectLogic.atomize_thm |> make_nnf;
 
-
-
-
 (*The cache prevents repeated clausification of a theorem, 
   and also repeated declaration of Skolem functions*)  (* FIXME better use Termtab!? *)
 val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table)
@@ -297,7 +284,7 @@
   end;
 
 (*Populate the clause cache using the supplied theorems*)
-fun skolem_cache ((name,th), thy) =
+fun skolem_cache ((name,th), thy) = 
   case Symtab.lookup (!clause_cache) name of
       NONE => 
 	(case skolem thy (name, Thm.transfer thy th) of