removed unused function repeat_RS
authorpaulson
Wed Dec 14 16:13:09 2005 +0100 (2005-12-14)
changeset 18404aa27c10a040e
parent 18403 df0c0f35c897
child 18405 afb1a52a7011
removed unused function repeat_RS
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_axioms.ML
     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  
     2.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Dec 14 06:19:33 2005 +0100
     2.2 +++ b/src/HOL/Tools/res_axioms.ML	Wed Dec 14 16:13:09 2005 +0100
     2.3 @@ -25,7 +25,6 @@
     2.4    val clause_setup : (theory -> theory) list
     2.5    val meson_method_setup : (theory -> theory) list
     2.6    val pairname : thm -> (string * thm)
     2.7 -  val repeat_RS : thm -> thm -> thm
     2.8    val cnf_axiom_aux : thm -> thm list
     2.9    val cnf_rules1 : (string * thm) list -> string list -> (string * thm list) list * string list
    2.10    val cnf_rules2 : (string * thm) list -> string list -> (string * term list) list * string list
    2.11 @@ -58,8 +57,6 @@
    2.12  fun add_EX tm [] = tm
    2.13    | add_EX tm ((x,xtp)::xs) = add_EX (HOLogic.exists_const xtp $ Abs(x,xtp,tm)) xs;
    2.14  
    2.15 -
    2.16 -
    2.17  fun is_neg (Const("Trueprop",_) $ (Const("Not",_) $ Free(p,_))) (Const("Trueprop",_) $ Free(q,_)) = (p = q)
    2.18    | is_neg _ _ = false;
    2.19  
    2.20 @@ -136,13 +133,6 @@
    2.21  
    2.22  (**** Transformation of Clasets and Simpsets into First-Order Axioms ****)
    2.23  
    2.24 -(* repeated resolution *)
    2.25 -fun repeat_RS thm1 thm2 =
    2.26 -    let val thm1' =  thm1 RS thm2 handle THM _ => thm1
    2.27 -    in
    2.28 -	if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
    2.29 -    end;
    2.30 -
    2.31  
    2.32  (*Transfer a theorem into theory Reconstruction.thy if it is not already
    2.33    inside that theory -- because it's needed for Skolemization *)
    2.34 @@ -265,9 +255,6 @@
    2.35         |> transform_elim |> Drule.freeze_all
    2.36         |> ObjectLogic.atomize_thm |> make_nnf;
    2.37  
    2.38 -
    2.39 -
    2.40 -
    2.41  (*The cache prevents repeated clausification of a theorem, 
    2.42    and also repeated declaration of Skolem functions*)  (* FIXME better use Termtab!? *)
    2.43  val clause_cache = ref (Symtab.empty : (thm * thm list) Symtab.table)
    2.44 @@ -297,7 +284,7 @@
    2.45    end;
    2.46  
    2.47  (*Populate the clause cache using the supplied theorems*)
    2.48 -fun skolem_cache ((name,th), thy) =
    2.49 +fun skolem_cache ((name,th), thy) = 
    2.50    case Symtab.lookup (!clause_cache) name of
    2.51        NONE => 
    2.52  	(case skolem thy (name, Thm.transfer thy th) of