src/HOL/Tools/Sledgehammer/clausifier.ML
changeset 38652 e063be321438
parent 38632 9cde57cdd0e3
child 38795 848be46708dc
     1.1 --- a/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Aug 23 14:51:56 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/clausifier.ML	Mon Aug 23 14:54:17 2010 +0200
     1.3 @@ -7,7 +7,6 @@
     1.4  
     1.5  signature CLAUSIFIER =
     1.6  sig
     1.7 -  val transform_elim_theorem : thm -> thm
     1.8    val extensionalize_theorem : thm -> thm
     1.9    val introduce_combinators_in_cterm : cterm -> thm
    1.10    val introduce_combinators_in_theorem : thm -> thm
    1.11 @@ -25,7 +24,7 @@
    1.12  (* Converts an elim-rule into an equivalent theorem that does not have the
    1.13     predicate variable. Leaves other theorems unchanged. We simply instantiate
    1.14     the conclusion variable to False. (Cf. "transform_elim_term" in
    1.15 -   "ATP_Systems".) *)
    1.16 +   "Sledgehammer_Util".) *)
    1.17  fun transform_elim_theorem th =
    1.18    case concl_of th of    (*conclusion variable*)
    1.19         @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
    1.20 @@ -78,10 +77,6 @@
    1.21  
    1.22  (**** REPLACING ABSTRACTIONS BY COMBINATORS ****)
    1.23  
    1.24 -(*Returns the vars of a theorem*)
    1.25 -fun vars_of_thm th =
    1.26 -  map (cterm_of (theory_of_thm th) o Var) (Thm.fold_terms Term.add_vars th []);
    1.27 -
    1.28  val fun_cong_all = @{thm expand_fun_eq [THEN iffD1]}
    1.29  
    1.30  (* Removes the lambdas from an equation of the form "t = (%x. u)".